proofs VS dafny

If you're already familiar with a functional programming language like Haskell or OCaml, you have the prerequisite knowledge to work through my Coq tutorial here: https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

My goal with this tutorial was to introduce the core aspects of the language (dependent types, tactics, etc.) in a "straight to the point" kind of way for readers who are already motivated to learn it. If you've heard about proof assistants like Coq or Lean and you're fascinated by what they can do, and you just want the TL;DR of how they work, then this tutorial is written for you.

Any feedback is appreciated!

Personally I treat Coq like an extension of my brain. Whenever I'm uncertain about something, I formalize it in Coq. I have a repository of proofs with GitHub Actions set up in such a way forbids me from pushing commits containing mathematical mistakes. I've formalized various aspects of category theory, type theory, domain theory, etc., and I've also verified a few programs, such as this sorting algorithm. Lately I've been experimenting with a few novel types of graphs, proving various properties about them with the aim of eventually developing a way to organize all of my data (files, notes, photos, passwords, etc.) in some kind of graph structure like that.

It's always a pleasant surprise to see people using Coq and other formal verification technology. We need more rigor in programming! If this article gave you a thirst for interactive theorem proving and you want to learn it from the ground up, I've recently written a Coq tutorial [1] which covers topics like programming with dependent types, writing proofs as data, and extracting verified code. That repository also contains a handy tactic called `eMagic` [1] (a variant of another useful tactic called `magic` which solve goals with existentials) which can automatically prove the theorem from the article.

[1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

[2] https://github.com/stepchowfun/proofs/blob/56438c9752c414560...

For anyone who wants to learn Coq, I've just finished writing a tutorial [1] that is aimed at programmers (rather than, say, computer scientists). It covers topics like programming with dependent types, writing proofs as data, universes & other type theory stuff, and extracting verified code—with exercises. I hope people find it useful, and any feedback would be appreciated!

[1] https://github.com/stepchowfun/proofs/tree/main/proofs/Tutor...

Hi all, Coq is a "proof assistant" that allows you to write both code and proofs in the same language (thanks to the Curry–Howard correspondence). Its uses range from pure math (e.g., the Feit–Thompson theorem was proven in Coq!) to reasoning about programming languages (e.g., proving the soundness of a type system) to writing verified code (e.g., this verified C compiler!). You can "extract" your code (without the proofs) to OCaml/Haskell/Scheme for running it in production. Coq is awesome, but it's known for having a steep learning curve (it's based on type theory, which is a foundational system of mathematics). It took me several years to become proficient in it. I wanted to help people pick it up faster than I did, so I wrote this introductory tutorial. Hope you find it useful!

Automation of Hoare logic is quite good these days. Dafny, from MS Research (https://dafny.org), is probably the most friendly formal language. Dafny has been used to verify large systems, including many components of AWS. I am hoping that LLMs make more advanced languages, such as Liquid Haskell or Agda, much easier to write. Ideally, lots of code should be autocompleted once a human provides a type signature. The advantage of formal verification is that we are sure the generated code is correct.

Modern software verification employs various approaches, each offering different trade-offs between ease of use and strength of guarantees. AWS contributes to the open source program verification tools used in the previous examples. Dafny and Kani represent two powerful approaches to program verification. Let's see how they work in practice before connecting the dots between automated reasoning and generative AI.

On that note, I discovered Dafny[1] recently, as a more accessible way to program with proofs. There's a companion book[2] that seems very accessible and down-to-earth (and, unfortunately, quite expensive). I didn't have the time to play with it yet, but it looks like it does what Ada/SPARK does (and more), but with less verbose syntax and more options for compilation targets. It seems to be actively developed, too. Personally, I had a very hard time getting into Coq, which is a proof assistant more than a programming environment - Dafny seems much more welcoming for a "working programmer" :)

[1] https://dafny.org/

[2] https://mitpress.mit.edu/9780262546232/program-proofs

https://dafny.org/ also allows proof checking and allows do write real programs with it. It has a java like syntax and is also from MS I believe

> I do think there's a bit of the Ignaz Semmelweis[1] issue at hand here, where developers want to believe in their inherent quality and refuse processes that improve safety if it goes against their worldview

I think the problem is that other variables (not only safety) must be assessed beyond the pure "better". Haskell is very good also. Very correct. Who uses that, and where? And why? Why not everyone uses https://dafny.org/ ?

For those that are interested but perhaps not aware in this similar project, Dafny is a "verification-aware programming language" that can compile to rust: https://github.com/dafny-lang/dafny

Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model.

C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead.

The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5].

[1] https://www.microsoft.com/en-us/research/project/code-contra...

[2] https://github.com/Z3Prover/z3

[3] https://github.com/microsoft/CodeContracts

[4] https://github.com/dafny-lang/dafny

[5] https://github.com/dotnet/csharplang/issues/105