Re: [Caml-list] Unsoundness is essential

[skaller <skaller@users.sourceforge.net>]

On Thu, 2007-10-04 at 14:45 +0200, Vincent Hanquez wrote:
> On Thu, Oct 04, 2007 at 12:26:53PM +0100, David Allsopp wrote:
> > Personally, whenever I go back to C, the novelty of the relaxed type
> > system is instantly worn away on the first tricky-to-repeat core dump... at
> > least an Ocaml exception has a cat in hell's chance of being found
> > systematically!
> 
> That's sadly not true. GC bugs in some bindings are usually hard to find !

I think David's point is that many faults in C are diagnosed,
if at all, by a very hard to analyse output (a core dump).
Whereas in Ocaml more bugs are caught at compile time, and,
often a bug at run time has some simple abstract information
such as an exception constructor name, which help in pinpointing
the problem.

I don't think the claim was *elimination* as much as *improvement*.

However I thin David is missing my argument if he's thinking I am
arguing for a more relaxed type system: on the contrary I want an
even tighter type system. The problem is that the cost is likely
to be unsoundness -- in the process of making the type system
more expressive, we're bound to be forced to let some ill-typed
programs through because it is no longer feasible to prove
well-typedness in all cases.

My argument is that this just isn't a problem to worry about:
the only difference is that existing buggy programs which
were previously judged type correct, are no longer decided
as type correct. In some cases a program will be let through
by BOTH type systems, and in others the more expressive 
system will find the error, so the fact that the type system
is unsound is not a problem: our confidence in the correctness
of the program is *enhanced* despite the unsoundness.

Furthermore, my program which today is accepted may be rejected
tomorrow when a theorist finds some way to reduce the unsoundness
by catching more cases. This is impossible if you don't let me
write the annotations just because you can't prove the well
typedness right now!

BTW: when I say 'type system' and 'soundness' I mean
*static type checking*. I do not consider dynamic typing
as a type system in this sense. Any type test at run time
is instant proof of unsoundness of the type system:
an ill typed program has been allowed to escape to run time.

The fact that a policeman is set to catch the inmate who
escaped from jail does not in any way diminish the fact
the inmate indeed escaped, and the jail security system
was unsound (Ouch .. new season of Prison Break .. :)


-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net