Re: [Caml-list] Unsoundness is essential

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

On Thu, 2007-10-04 at 17:29 +0200, Andrej Bauer wrote:

> 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

Yes, I want something like that.

> This I would call "controlled unsoundness" 

As an (eX) motorcyclist I can agree .. riding a bike is like
having one continuous controlled road accident.. :)

> 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.

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.

If you can produce a compiler with an expressive type system
but cannot yet create a complete list of unproven assertions,
that is still better than writing Python. In fact I write a lot
of Python even now. I do not do so in ignorance of the value
of static type checking! There is a good reason I choose it,
for example for the Felix build system.

It is not because I fear writing all the types Ocaml would
require, but because the need for 'dynamic typing' in this
kind of software and the lack of expressiveness in Ocaml
type system makes Ocaml unsuitable. Please note I'm *trying*
to explain the reason, but probably haven't got it right.

The point is, in the manifesto it should go like: expressiveness
first, then generating proof obligations, and also with time,
improving the automatic provers. 

The key thing is not to restrict expressiveness just because
the type system cannot fully cope.. making the typing more
expressive has many benefits by itself.

A stupid one: how can theoreticians test the efficacy of a new
algorithm with real world case data?


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