Martin Kleppmann

It takes a long time to

learn the language of writing those proofs.

And then even once you know the language, it's just really laborious in order to actually write the individual proof steps.

Yeah, so you're trying to make a proof that a certain piece of code always satisfies a certain property.

In some cases, that property might be quite easy to specify.

Let's say as a really simple example, you have two lists and you want to concatenate them.

And then you want to prove that the length of the concatenated list equals the sum of the two individual lists.

Very, very simple property.

How would you prove something like this?

Well, you would have a function that concatenates two lists, and then you would probably do a proof by induction over one of the lists that shows that, okay, well, if you have one list of length i and another list of length 0, well, then the sum of the two is i. If you have a list of length i appended with a list of length 1,

well, then it's i plus 1 and so on.

And then by using a proof by induction, you can then show that the length of the concatenated list is i plus j, where i and j are the lengths of the two input lists for every possible value of i and j. And this is something that, you know, in a test case, you would, in tests, you would maybe test it for the cases of j equals 0, j equals 1, and j equals 5, and then you're done.

And j equals interior max.

Yes.

In the edge case, if that's what we do, that's how I write my unit test.

Exactly.

And so this is a trivial example, like list concatenation.

You can easily just read the code and convince yourself that it's correct.

But if it's a much more complex algorithm, then our brains just can't like grok the algorithm well enough to really convince ourselves that it's correct if you don't prove it.

And that's where these proofs then become handy.