Re: [Caml-list] Unsoundness is essential

[Arnaud Spiwack <aspiwack@lix.polytechnique.fr>]

> Sure, but my point does remain: the expressiveness is more or less
> paramount. It is not so much that I personally desire it or not,
> but that real programmers in the real world go out there and do
> whatever is necessary to make programs work.
>   
That would be wonderful if they did work... Unfortunately to my 
knowledge, a software is a mere collection of bugs, glued together with 
a couple of features. Or perhaps I'm being a little optimistic here :p .
> A stupid one: how can theoreticians test the efficacy of a new
> algorithm with real world case data?
>   
This is obviously not possible (if I understand the question) since real 
world data don't obey any known law. However they can be modelized for 
further use.

Anyway that is not what you were talking about and I think the 
discussion got confused due to the wild mix of different notions. One 
interpretation of what you suggest is to replace pieces of proof by 
run-time assertions, this sounds a plausible idea, though this is 
probably not a good thing to do for a finished product. It could however 
allow the program to be tested before one tries to prove it. There are 
various other ways to do it, though.

Anyway, just be aware that having a more powerful type system usually 
means much more program that type. Contrary to what you seem to fear.


Arnaud Spiwack