On 2/11/11 1:25 PM, Luke Palmer wrote:
I would like to see a language
that allowed optional verification, but that is a hard balance to make
because of the interaction of non-termination and the evaluation that
needs to happen when verifying a proof.
I believe that ATS (short for Advanced Type System) allows this.
Although I haven't actually programmed in it, I read through the
documentation and it looks to me like it is a fully dependently-typed
language that allows you prove as little or as much about your program
as you like.
http://www.ats-lang.org/
Cheers,
Greg
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
