So, you're saying that the code would be less reliable if there was no work to prove it formally? Of course you aren't. What you're saying is that proving code is correct is insufficient. Of course it is insufficient. Your comment adds nothing to the debate.
What I'm saying is that asking that mathematicians produce their proofs in a form amenable to mechanical checking is like asking programmers to produce their code in a form that is amenable to mechanical checking. It's long, tedious, error-prone in its own right, and simply not going to happen. It's like asking people who write multi-million line programs in high-level languages to get the same functionality by writing in assembler.
Programming doesn't happen like that, and proofs don't either.
And your comment adds nothing to the debate while picking on a joke.
"is like asking programmers to produce their code in a form that is amenable to mechanical checking. It's long, tedious, error-prone in its own right, and simply not going to happen"
But programs are done in a form that's subject to mechanical checking. Compilers do that and only compile code that adheres to a strict syntax and grammar. In a higher level there are static code analysers that look for other defects. Some of them are in compilers already for optimization purposes.
Also, semiconductor companies use automated checkers for the inner parts of their processors, like floating point multipliers to make sure they are correct.
But running code through a compiler is akin to making sure the statements in a proof "make sense." The proof as a whole can be complete rubbish, which still making sense at a page by page level. I can't work out if you're trolling, or if you really don't understand my point.
A lot of undergraduate mathematics has been converted into forms that automated proof checkers can work with, and have verified. But new math just isn't like that. It's not yet well understood, it's got small gaps and bits that are wrong in inconsequential ways, and it's got an over-arching sense of purpose and meaning. Trying to convert a recently produced proof into a form amenable to checking is just not going to happen, and by the time it is understood well enough, and completed to a sufficient level of detail to make it possible in a sensible amount of time, it's pretty much pointless.
"But running code through a compiler is akin to making sure the statements in a proof "make sense." The proof as a whole can be complete rubbish, which still making sense at a page by page level."
Correct. But if one statement is incorrect then the proof is wrong, at least until that statement is corrected.
So it's only a partial verification, but you can be sure that if that points to an error, you still have work to do.
Code analyzers are getting better everyday but in the end it depends on what you want the code to do, so you would need to add an annotation "prove this function calculates 2*x for parameter x" for a complete proof
" Trying to convert a recently produced proof into a form amenable to checking is just not going to happen, and by the time is is understood well enough, and completed to a sufficient level of detail to make it possible in a sensible amount of time, it's pretty much pointless."
And that's where I disagree. If you can have your new theorem
in a machine readable/verifiable format, then other theorems can make use of it.
The idea is not to redo the work every time for a new theorem. I understand new math is much more complex, and that's why we should be thinking of making this available in a theorem prover.
It's certainly a very complex work and maybe not doable today, but it would have a big impact.
>> The proof as a whole can be complete rubbish, which
>> still making sense at a page by page level."
> Correct. But if one statement is incorrect then the proof
> is wrong, at least until that statement is corrected.
The statement-by-statement work is not only trivial, it's an important step to getting your head in the right place to understand where things are going, and why. Fixing the problem of making sure each statement is, in effect, syntactically correct is not just solving the wrong problem, it's solving a non-problem.
>> Trying to convert a recently produced proof into a form amenable
>> to checking is just not going to happen, and by the time it is
>> understood well enough, and completed to a sufficient level of
>> detail to make it possible in a sensible amount of time, it's
>> pretty much pointless.
> And that's where I disagree. If you can have your new theorem in
> a machine readable/verifiable format, then other theorems can make
> use of it. The idea is not to redo the work every time for a new
> theorem. I understand new math is much more complex, and that's why
> we should be thinking of making this available in a theorem prover.
It's being done now, but the problem is that producing new work, new theorems, is not going to be done within the framework of the automated system, because that's not where the meaning lives. When I produce a new proof, the fastest thing to do is to make it readable by other mathematicians, not convert it painstakingly to a different notation for a machine to check. That can, and really should, only be done once it's understood conceptually by other mathematicians.
There are people working on this, and they are making great strides. I just get really frustrated when people think a) it's obvious that machine checking is the way to go, b) why don't mathematicians all work on producing their proofs in machine checkable form, c) I don't understand these proofs, so obviously machine checking is better, and d) it really can't be that hard - even I can see it's a good idea.
I have no doubt that this will change over the next 50 years, perhaps even over the next 20 years. Prediction is hard, especially about the future, and I'm not going to try. What I do know is that I honestly cannot see how I would work trying to use a machine readable form, or trying to use a proof assistant. So far they've not merely been unhelpful, they've actively stopped me from working at all. No doubt it will be different for people raised with and trained on the "modern" systems of 20 years from now.
> It's certainly a very complex work and maybe not doable today,
> but it would have a big impact.
Yes, yes it would. I don't know how much math you know, there's nothing in your profile, but if you have enough to have a go at contributing to one of the major pieces of work underway to make it happen, you could make your mark.
My math knowledge is certainly not very big, but maybe above average. Probably not enough to work on the state of the art of theorem provers today. Still, a fascinating subject.
What I'm saying is that asking that mathematicians produce their proofs in a form amenable to mechanical checking is like asking programmers to produce their code in a form that is amenable to mechanical checking. It's long, tedious, error-prone in its own right, and simply not going to happen. It's like asking people who write multi-million line programs in high-level languages to get the same functionality by writing in assembler.
Programming doesn't happen like that, and proofs don't either.