Hacker News Reader

On the list of "cool things also happen to employ Z3", definitely check out MS Dafny programming language: https://github.com/Microsoft/dafny

View on HN

Ivy [1] is another research language built around Z3. Slides from a recent presentation of the language are also available [2]. The concept of exploiting modularity to obtain decidable verification conditions is quite interesting. Plus, it compiles down to C++.

[1]: http://microsoft.github.io/ivy/

[2]: http://vmcaischool19.tecnico.ulisboa.pt/~vmcaischool19.daemo... (PowerPoint slides)

How does Dafny differ from Microsoft's F* (FStar)[1]?

[1] https://www.fstar-lang.org/

It is more C# like, and was used to write one of the Singularity post OSes at MS Research.

"Automated Verification of a Type-Safe Operating System"

https://www.microsoft.com/en-us/research/wp-content/uploads/...

Thanks. I see the F#/F* synergy. Are C#/Dafny as similar to favor them over the F#/F* combo?

Reply on news.ycombinator.com