[shawa_a_a]

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 [2] https://github.com/shawa/formal-verification-project

[thethirdone]

> 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]

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/). It's indeed used as a proof backend in several tools, including frama-C and Dafny (Microsoft Research), but otherwise it's from academia.