Re: [Caml-list] Unsoundness is essential

[Andrej Bauer <Andrej.Bauer@fmf.uni-lj.si>]

At the danger of repeating myself (for which I apologize), I would like 
to convince skaller that he does not want unsound type systems. (What 
skaller calls "sound" I call "safety property" in my previous post.)

Skaller, you want something like this:

(a) expressive power (dependent types, subsets, you-name-it)

(b) soundness, in the following form:
     * the compiler rejects obvious nonsense
     * the result of a compilation is a program and a list of
       assertions which the compiler was unable to verify

This I would call "controlled unsoundness" which at least allows the 
human to see what needs to be verified to guarantee soundness. It's much 
better than the sort of unsoundness that skaller seems to be advocating.

There is actually a new minor point I want to make: you cannot postpone 
all problems with typechecking to runtime. Only very simple conditions, 
such as bounds checks, can be checked at runtime.

It is very easy to come up with preconditions that are computationally 
unverifiable. For example, you might have a numerical method for 
zero-finding which only works if the input is a function satisfying a 
funky condition, e.g., "the function is convex". How are you going to 
check that at runtime?

Or to give you a much more simplistic example:

fun find_zero (f: int -> int where not (forall n:int, f(n) != 0)) {
   int i = 0;
   while (f(i) != 0) { i++; }
   return i;
}

How will you verify the precondition on f at runtime?  In this case I 
would expect the compiler to list all uses of find_zero applied to 
functions which are not known not have a zero. Let the human worry.

Andrej