4 ms·
I don't think the point is to either have good math or good code. When you develop software in Coq and the likes, it is library code. It is high impact code th
by madsbuch 3y ago
I don't think the point is to either have good math or good code.
When you develop software in Coq and the likes, it is library code. It is high impact code that is guaranteed to be correct. It is written once and not maintained – You would never build the new Twitter in Coq.
When you develop math on Coq, you build abstractions. You just need to know that theorems that you are working on. Then you pull in all the lemmas in coq to help you solve that theorem. You do not need to understand the lammas coq uses to help you prove your theorem – coq does that for you. So your math is extremely concise. This is in opposition to normal math, where you need to be able to explain the hierarchy your theorem works on top of.
- hgsgm 3y agoNormal math also concisely cites pre-existing theorems
- infogulch 3y agoAh but normal math is a social compact in a way that computer-aided proofs are not. Very few handwritten proofs are actually written down in detail, and there are various cases where attempting to do so actually failed or required new work to actually close the gap.
- trenchgun 3y agoProof assistants assist with normal math. They just make the normal formal and realiable.
- mcguire 3y ago"It is written once and not maintained..." Be careful, this is how you get the Ariane V first flight. "You do not need to understand the lammas coq uses to help you prove your theorem..." If I wanted to generalize your theorem or move it to some other base abstraction, the first thing I need to do is to read and understand your proof. If that proof is made up of Coq tactics chosen based on "whatever works", I'm going to have a bad day. Now, many results especially in CS are made by reducing a new problem to an existing theorem, but I don't know how well that works as a general case.