Re: [Caml-list] Unsoundness is essential

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

On Thu, 2007-10-04 at 13:02 -0700, Ken Rose wrote:
> skaller wrote:
> > It seems a consequence of this manifesto is that the asserting
> > of the assertions, if not their proofs, need to be encoded
> > into the program in an effort to reduce the size of the output
> > list.
> >
> > A difficulty here is saying the assertions in a comprehensible
> > way which is well coupled to the original code. As you said
> > previously, this probably requires an interactive system.
> >
> >   
> I think that in an industrial system, the assertions are going to have 
> to travel with the code.  I can't imagine that a system that needs a 
> particular, highly trained programmer (the one who wrote the thing) to 
> cajole the compiler into generating code will ever be satisfactory to 
> any business that writes code.

There is a such a system, I can't remember its name. The proofs and
types etc do travel with the code, but the 'language' is designed with
holes to fill in interactively, and the compiler fills them out
partially then prompts for the balance. After supply, more holes
are filled in by the same process.

So for export, you get a complete linear representation of 
the conventional kind but you use a GUI to develop it.
Perhaps someone can provide a link (it's quite well known
very advanced category theory based system).


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