What is Dafny?
Dafny is a programming language which is designed to help developers prove that their software is correct. Most consider this the domain of mission critical software where there are serious costs or consequences of software errors, but it can be used on everyday software as well!
If you are interested in learning why your software is correct or why it works, verifying it with Dafny will make it clear. It helps take your intuition about a program and make it rigorous.
Quite a lot of programming can be done with trial and error, but often it can be long and frustrating when you don't understand a system well and seemingly random permutations result in working code or not. Often, it can lead to doubt about whether a particular solution is always correct. Unit tests can help, but they can only prove the presence of bugs on specific examples.
A verified program is mathematically guaranteed to be correct on all valid input.
Why Dafny?
Dafny was developed by Rustan Leino, formerly of Microsoft Research. It is still under active development.
It has a similar syntax to C# or TypeScript or many other C inspired languages. It is a huge language with many powerful constructs that map to common situations and patterns in most common programming languages used today.
It's a practical language
There are other formal verification languages which are based on functional programming languages or type theory and pure logic. These languages can and are used to verify software, but if you want to verify a small piece of your web application you have to learn a completely different paradigm and syntax before you can get to doing something useful.
I find Dafny very approachable and familiar as a professional web developer.
Challenges ahead
As mentioned Dafny is still under development and the documentation is a bit lacking still. In that vain this series intends to provide many examples and explain how to verify different programs.
Familiarity with mathematics
Dafny can prove many things but often we must explain non-trivial properties to help Dafny verify our software. This is based on mathematical logic and induction. Dafny has a system and syntax specially designed to allows us to prove things to Dafny.
Unfortunately, Dafny cannot prove everything we want automatically and there are many sharp edges when we write our proofs in Dafny. However, it is a powerful system which beautifully brings the world of mathematics into an approachable and understandable context of software development.
Getting Started
Dafny is now easily packaged into a Visual Studio Code extension. Installing the extension and then creating a file with the .dfy extension will immediate set you into a dafny environment and you can begin writing and verifying your algorithm.
Go read and tryout the Dafny Getting Started Guide
Learning Dafny
After reading the guide, it is time to start practicing verification on simple coding problems. Here in this series we will implement and verify a large number of algorithms and coding problems.
Top comments (0)