Write a program to prove another one. It's pretty cool in concept, but is it useful in practice?
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.
Are you saying the practical relevancy here is actually to logicians? In that it means they can now more easily come up with proofs for their theorems by simply writing a program instead of whatever more complicated paper proof they used to have to come up with?
And that for software, it's only helpful in special cases where you need to guarantee a small piece of logic is 100% correct?
i'd say yes
Formal verification hasn't really caught on yet. The extra effort needed to formally prove even a trivial program seems to be too high for the value it gives to most stakeholders.
I'm really hopeful for simpler methods of formalized proofs, or even automated testing. I think today, the practical cost is maybe still too high for people to care.
On the other hand, formal construction is an idea whose time is long overdue. Rather than asking if program text T satisfies predicate P, instead start with P and then construct a T mechanically such that it must satisfy P. The latter is a much easier task than the former. Sort of like how it's easy to know N is the product of two large primes if you just multiplied two large primes together to get it.