#formal methods

Someone recently told me a project isn’t real until you do a retrospective, so I think it’s time to do one for Let’s Prove Leftpad. Short explanation: it’s a repository of proofs of leftpad, in different proof systems.

Long explanation: the rest of this post.

Background

I’m into formal methods, the discipline of proving software correct. Consider the following contrived code:

def add(x: int, y: int): int {   if(x == 12976 && y == 14867) {     return x - y;   }   return x + y; }

This typechecks, and any black-box unit test would find that add(x, y) == x + y. It would also pass property testing: if you randomly picked two 16 bit integers, you’d have to run something like 500 million tests to have a 10% chance of triggering the bug. A formal verification tool would fail the code 100% of the time, and pass it if only if it was always correct.

The tradeoff for this kind of power is difficulty: proving code correct is very, very hard to do. This is pretty widely accepted in the FM discipline. Outsiders, though, often assume that function programs are easier to prove correct than imperative programs. While this might be true for informal reasoning, it’s not that true for formal proof. To show this, in 2018 I made an online challenge to people:

Lots of people say "FP is easier to analyze than imperative code because of purity" but whenever I ask for evidence people look at me like I'm crazy. So I'd like to make a challenge: I'll provide three imperative functions, and your job is to convert them into pure functions.

Here's the catch: I formally proved all three functions are correct. You have to do the same. And by "formally prove", I mean "if there are any bugs _it will not compile_". Informal arguments don't count. Quickcheck doesn't count. Partial proofs ("it typechecks") don't count.

I provided two warmups, leftpad and unique, and a main challenge, called “fulcrum”. The full details and results are documented here.

Two things came out of the theorem showdown. First, it put me in touch with Lars Hupel, and we’ve been fast friends ever since. Second, this tweet:

And that’s when I realized that leftpad is a great proving exercise.

A short, sweet argumentation for why formal methods / TLA+ might be useful for you. Based on a number of short use cases.

Creusot is a tool for deductive verification of Rust code. It allows you to annotate your code with specifications, invariants and assertions and then check them formally, returning a proof your code satisfies its specification.