[Haskell-cafe] Proving correctness

Gregory Crosswhite gcross at phys.washington.edu
Tue Feb 15 04:07:39 CET 2011

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.



More information about the Haskell-Cafe mailing list