14 Feb
2011
14 Feb
'11
10:07 p.m.
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