Martin Kleppmann

Yeah, so there's a whole range of formal methods.

One approach is to, for example, use a specification language like FISB or TLA Plus or something like that to describe the expected behavior of a system at a high level and then use a model checker, which is essentially like a randomized test case generator to just play through a lot of scenarios and see whether the system has those desired behaviors in all the different scenarios.

That's like the sort of intro level formal verification, I would say.

The more advanced level is to use actual formal proof.

And in that case, you can write a specification of some system in a formal language as usually using mathematical notation.

and then make a mathematical proof that a certain algorithm or certain implementation always satisfies that specification.

And the distinction to testing there is that, well, in testing, you just try through a couple of examples, give the algorithm some example inputs and check whether you get the expected output in those particular examples.

But a proof can reason about potentially infinite state spaces.

So it can tell you things about like

every possible thing that could possibly happen in the entire universe showed that, for example, a certain safety property is always given in those.

Formal verification is a lot of work.

I never used it in my time in industry because it's just too time-consuming, basically.

I only got into formal verification when I was in academia, and I could afford to take the time to spend a few months proving an algorithm correct.

But there I've

I started finding this very useful, especially if I was working on very subtle algorithms where it's very hard to tell just from reading the implementation whether this actually is always correct under all possible cases.

But if it's an important algorithm where, for example, it will corrupt data if there's a mistake in it, or it will have a security vulnerability if there's a mistake in it,

then when it's high stakes, things like that, then I feel it's worthwhile to have formal verification and to really make sure that the code really is correct.

And so I've done some formal proofs using the Isabel proof assistant, for example.

There are a couple of others as well, like Rock and Lean and so on.

These proofs are really hard to write.