[bsaul]

in practice, what kind of proof are people building when building real world programs ?

Are people writing only top level assertion ( such as "this main function always terminate") and the checker points at all the gaps ?

Or does one has to write proofs for every single intermediate layer and functions ?

In wich case, do people then have access to prebuilt "proven functions" in a stdlib ? such as "NeverEmptyList" or "AlwaysGreaterThanXVariable" ?

[nickdrozd]

> in practice, what kind of proof are people building when building real world programs ?

Here's an example of a proof from a Turing machine simulator written in Idris [1]. The claim is that the length of the tape never decreases after taking a step.

The "claim" is stated in the type signature, and the "proof" is an implementation of that type. That's what "propositions as types" means. The whole thing looks like a regular function, except that it doesn't do anything and it never gets called. However, by virtue of having been accepted by the type-checker it verifies the claim about that piece of the program's behavior.

[1] https://github.com/nickdrozd/rado/blob/86790bbb218785e57ea88...

[jacobparker]

Some examples from a Software Foundations (a series of books about Coq, available online):

I just wrote something I called insertion sort. I want to know that this is a valid implementation of sorting. What does it mean to be a sorting algorithm? It means that the output is sorted, and it's a permutation (shuffling) of the input. This is an exercise here: https://softwarefoundations.cis.upenn.edu/vfa-current/Sort.h...

Say I've written a Red-Black tree. I want to know that it behaves like a map, or that it keeps the tree appropriately balanced (which is related to performance): https://softwarefoundations.cis.upenn.edu/vfa-current/Redbla...

One more: say you have specified a programming language, which includes describing the structure of programs (the grammar essentially) and "small step" semantics (e.g `if true then x else y` can take a step to `x`). It would be interesting to show that any well-typed halting program can be evaluated in multiple steps to exactly one value (i.e. the language is deterministic and "doesn't get stuck" (or, in a sense, have undefined behaviour)). That's the subject of volume 2 https://softwarefoundations.cis.upenn.edu/plf-current/toc.ht... Beyond this, you may have done a similar thing for a lower level language (machine assembly, wasm, ...) and have a compiler from your language to the low level language. You may want to prove that the compiler "preserves" something, e.g. the compiled output evaluates to the same result ultimately.

RE: termination, in something like Coq that is a bit special because every function terminates by construction. That might sound limiting but it's not really/there are ways around it. It would, however, be impossible to write something like the Collatz function in Coq and extract it in the obvious sense.

EDIT: and there are other ways these tools can (theoretically) be used to work with programs, but that's a long story. There have been real-world programs built like this, but it is very uncommon at this time. It is an area of active research.

[kragen]

Hey, thank you very much for these pointers! SF is one of those things I keep meaning to get around to. Just yesterday I was trying to figure out how I'd go about proving a binary search correct.

[jacobparker]

I highly recommend SF. The trick is you must use the books via coqIDE or something equivalent; viewing the rendered HTML is almost pointless at best, but probably counter-productive.

Binary search would be a good exercise. I think SF volume 1 would be more than enough, with the exception of deciding how to model arrays (you'd probably want to look up Coq's persistent arrays/PArray system for this.) SF volume 3 does binary search _trees_ which is similar but avoids the array problem (as is customary in functional languages.)

However, Coq (by default) also uses infinite precision numbers. This works very well for proofs but isn't necessarily realistic. This is where some extra fun comes in: fixed precision arithmetic is a very common source of bugs for binary search: https://ai.googleblog.com/2006/06/extra-extra-read-all-about...

[kragen]

Thank you! What was your formal-methods background before you tackled SF?

[whateveracct]

It depends? But it's nice to have the option.

DTs doesn't mean everything is proven to the max.

Haskell already has a proven `NonEmpty` list without DTs - you can prove that with a product type alone :)

And that proof is useful because it allows you to have better proofs down the line. For instance, the min or max of a NonEmpty always exists. But the min/max of a list can be Nothing.

[amw-zero]

Here’s a talk where someone shares proofs within the sel4 verified OS project: https://youtu.be/AdakDMYu4lM.