This isn't necessarily about proving other programs. It is about showing that at a very fundamental level, formal logic (as studied by logicians) and typed prog

This isn't necessarily about proving other programs. It is about showing that at a very fundamental level, formal logic (as studied by logicians) and typed programming languages (as studied by computer scientists) are actually the same thing, but written in different ways. The basic idea is that there every typed programming language is analogous to a mathematical logic system and that * programs are analogous to logic statements (theorem) * a program's source code is equivalent to a proof of the theorem. * type-checking a program is equivalent to checking if a proof is correct. * Executing a program is equivalent to simplifying a proof. If we restrict ourselves to the sort of type systems in mainstream languages the logic statements that the types can express are somewhat limited and not very interesting. The proofs as programs analogy really starts getting interesting when you have a very powerful type system... One place where you see these powerful type systems is in the proof assistants for people who want to formalize mathematics. It turns out that writing proofs on these proof assistants is surprisingly similar to programming in a typed functional language! It is kind of interesting because all that you care about is that the program you write (the proof) type checks (is valid), and you don't actually ever run it. Coming closer to the software development side of things, some of these proof assistants can be used to produce formally verified software. Basically, what they do is that instead of throwing away the programs (proofs) that you write, they compile them down to executable code. This is not something that is very applicable to the general software population though since formal verification is a niche thing. It also doesn't help that these tools are currently super clunky to use and have a steep learning curve involving lots of difficult math.