Dafny is a verification-aware programming language

I think compact verification aware languages will be of particular interest to anyone wanting to make machine learning models write code at scale. Verification, and test generation, seem critical to the process of getting feedback from the program itself and improving the automatic code generation process. Not quite as powerful as self-play was for two player game playing, but it's got to be close.

fyi Dafny is written by Microsoft and used by Amazon: <a href="https:&#x2F;&#x2F;www.amazon.science&#x2F;blog&#x2F;how-we-built-cedar-with-automated-reasoning-and-differential-testing" rel="nofollow">https:&#x2F;&#x2F;www.amazon.science&#x2F;blog&#x2F;how-we-built-cedar-with-auto...</a>

I&#x27;ve tried a few times to get into this but honestly it&#x27;s very very difficult. You pretty much need to have a degree in formal verification to be able to actually verify anything except toy examples. I kept hitting cases where things wouldn&#x27;t verify, and the reason is due to something deep in the implementation that really only the authors would know about.<p>Also the language is huge, and while it&#x27;s quite well documented, the level of documentation you <i>want</i> for this is far more than for a normal language.<p>On the plus side, the authors are really helpful on Github, and the IDE support in VSCode is great.

Looks like a cornucopia of nice programming language features, including one that&#x27;s in Ada that almost no other language provides: integer subset types&#x2F;range types. Definitely promising.<p>The documentation is very jittery&#x2F;laggy while scrolling on a phone though. I don&#x27;t know why that&#x27;s about, but it&#x27;s distracting.

There&#x27;s a recent textbook for Dafny aimed at undergraduates with a bit of programming experience. [0]<p>[0] <a href="https:&#x2F;&#x2F;mitpress.mit.edu&#x2F;9780262546232&#x2F;program-proofs&#x2F;" rel="nofollow">https:&#x2F;&#x2F;mitpress.mit.edu&#x2F;9780262546232&#x2F;program-proofs&#x2F;</a>

Looks like it has been around since 2008:<p><a href="https:&#x2F;&#x2F;www.microsoft.com&#x2F;en-us&#x2F;research&#x2F;project&#x2F;dafny-a-language-and-program-verifier-for-functional-correctness&#x2F;" rel="nofollow">https:&#x2F;&#x2F;www.microsoft.com&#x2F;en-us&#x2F;research&#x2F;project&#x2F;dafny-a-lan...</a><p>&gt; K. Rustan M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR-16, volume 6355 of LNCS, pages 348-370. Springer, 2010.<p>&gt; K. Rustan M. Leino. Specification and verification of object-oriented software. In Engineering Methods and Tools for Software Safety and Security, volume 22 of NATO Science for Peace and Security Series D: Information and Communication Security, pages 231-266. IOS Press, 2009.

Very neat. Needs Rust compilation support!