[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...