I agree with this wholeheartedly. The down side is that it's going to take forever to get everyone on board. Mathematicians are very hostile to outside influences.
Constructive mathematics should be more of a thing too.
Constructive mathematics should be more of a thing too.
Many years ago, around 1980, I headed a project to build one of the first program proof of correctness systems. (It's on Github now, about two-thirds working with modern compilers.)[1] We succeeded, but it was just too hard to use. And, back then, really slow. As in 15 minutes to hours.
We had two theorem provers. One was what's now called an SMT solver - it could prove theorems with addition, subtraction, multiplication by constants, equalities, inequalities, and the Boolean operators. It could also accept rewrite rules, which it accepted as true.
Because allowing users to input rewrite rules made it easy to create false proofs, we required that the rewrite rules be proven using the Boyer-Moore theorem prover, which is a pure constructive system.[2] Then the theorems could be transferred to the SMT solver and used there.
One of the things we set out to prove were the "axioms" for arrays. There are four, credited to McCarthy in his classic 1962 paper. But we wanted to prove them from a theory of constructive arrays. In Boyer-Moore theory, we defined arrays as sorted lists of (subscript, value) tuples. And then we set out to prove the classic four axioms for arrays with machine proofs.
Which we did.[3], starting at line 3372. That file is the Boyer-Moore theorem prover grinding its way up from a very low base of number theory to the theorems we needed for our program proving system. (On a modern computer, in seconds. Took 3 hours on a VAX in 1980. We just didn't have enough engine for this stuff back then.) In that notation, "(selecta A I)" means A[I], and "(storea A I V)" is array A with A[I] replaced with V. After some struggles, we got the the prover to find a way to prove that.
But it's ugly. There's lots of case analysis, which mathematicians hate. We didn't get to redefine "equal", so we couldn't have abstract sets. We had to have ordered lists of tuples, which meant all the fussyness of updating an ordered list representation and proving that was sound. But it all worked.
So I submitted this to JACM, back when that mattered. It was rejected. The comments were along the lines of "I don't like having something that ugly at the foundations of computer science". The reviewers all agreed it was valid, but they just didn't like doing it that way, in an automatic but inelegant way.
Looks like the author of the original article here is still having that problem.
Good times back then. But we were way ahead of our time.
[1] https://github.com/John-Nagle/pasv
[2] https://github.com/John-Nagle/nqthm
[3] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
True or false – if x is a real number,
and x² − 3x + 2 = 0, then x = 1.”
My answer “False – set x = 2.
Lean: “OK, so it now suffices to prove that
(a) 2² − 3×2 + 2 = 0 and that
(b) 2 ≠ 1.
So, you rather give your users something bug free in which they can express the basics of numbers, starting, for example, with the Peano axioms (https://en.wikipedia.org/wiki/Peano_axioms) (and that isn’t even the bottom of the stack; an even more basic system could replicate Principia Mathematica (https://en.wikipedia.org/wiki/Principia_Mathematica))
It’s a long road from there to high school math and an even longer one to mathematics research, so users not only will be able to do the above, but they will have to, if they want to do something at the front of mathematics.
I (I'm not the only one) think that Hilbert was wrong.
Programming is a whole discipline apart from mathematics. It's grounded in mathematics, but in practice it really is engineering. There are myriad choices to be made, most of little or no mathematical significance. Just managing names becomes a task; using the same Hebrew letter to mean five (more or less analogous) things in one proof becomes impossible. Maybe even using a Hebrew letter is hard.
Mathematicians who wanted to be programmers might be programmers already. Mathematicians willing to do engineering might be engineers already.
We have lots of experience with physics grad students writing unmaintainable spaghetti code to analyze experimental result data. It is tolerable because the code is more-or-less discarded after the paper is published. But this code is supposed to support all of the future of mathematical development, forever.
Who will rewrite the shoddy parts when their (practical) flaws become intolerable? Will it even be possible, with the weight of decades depending on it? What abstraction methods does the language offer to help decouple the statement proven from the expression of its proof?
Very often the lemma your proof depends on isn't exactly what somebody else proved, but something analogous. Mutatis mutandis, it's the same, conceptually, but that's not good enough for your proof system.
Do you want dozens of almost-identical proof statements in the system? Is the language strong enough to unify them? Does unifying them count as doing maths? It will usually feel more like engineering.
Other software engineering considerations become important, notably runtime performance. Is a proof acceptable if it would take a hundred years to evaluate, so hasn't been? Can it be parallelized? Who provides the equipment to do it?