3 ms·

To throw another one onto the _have you looked at X_ pile, Microsoft Research has put a lot of effort into the Why3 theorem proving platform, which is the backe

To throw another one onto the _have you looked at X_ pile, Microsoft Research has put a lot of effort into the Why3 theorem proving platform, which is the backend for the verifier built into their (experimental?) verifier-aware, imperative language, Dafny[1]. It feels very much like writing C#/Java but with verified pre/post conditions, loop invariants etc. I took a formal verification course in college that involved writing several verified sorting, search etc. algorithms in Dafny [2]. I remember it being somewhat cumbersome to write your assertions in a way that the checker can check them, but it's looks very much like what you're suggesting. (At the time I didn't realise that not only does the checker check the program, but compiles it into a CLR-compatible binary, hence you'll see equivalent C code for comparison) [1] https://github.com/Microsoft/dafny https://github.com/Microsoft/dafny [2] https://github.com/shawa/formal-verification-project https://github.com/shawa/formal-verification-project

c-cube 9y ago
Just to give credit where it's due, I believe why3 is developed purely by LRI, a public french research lab (see http://why3.lri.fr/ http://why3.lri.fr/). It's indeed used as a proof backend in several tools, including frama-C and Dafny (Microsoft Research), but otherwise it's from academia.
thethirdone 9y ago
> To throw another one onto the _have you looked at X_ pile, I am pretty sure I have seen Dafny before, but it wasn't on the top of my head. Thanks for mentioning it. > I remember it being somewhat cumbersome to write your assertions in a way that the checker can check them, but it's looks very much like what you're suggesting. I agree with both of those statements. I am not thinking of something revolutionary. I have been thinking of a few ways to make it more ergonomic than Dafny though. Refinement types would be one of the key ways to do that. I think all of the key capabilities would be the same though. It would probably make sense to make a transpiler to Dafny to try it out.

c-cube 9y ago

Just to give credit where it's due, I believe why3 is developed purely by LRI, a public french research lab (see http://why3.lri.fr/ http://why3.lri.fr/). It's indeed used as a proof backend in several tools, including frama-C and Dafny (Microsoft Research), but otherwise it's from academia.

thethirdone 9y ago

> To throw another one onto the _have you looked at X_ pile, I am pretty sure I have seen Dafny before, but it wasn't on the top of my head. Thanks for mentioning it. > I remember it being somewhat cumbersome to write your assertions in a way that the checker can check them, but it's looks very much like what you're suggesting. I agree with both of those statements. I am not thinking of something revolutionary. I have been thinking of a few ways to make it more ergonomic than Dafny though. Refinement types would be one of the key ways to do that. I think all of the key capabilities would be the same though. It would probably make sense to make a transpiler to Dafny to try it out.