in reply to
Re^4: OT: Mathematics for programming (again)
in thread OT: Mathematics for programming (again)
Alright, say you program a computer to verify a hairy proof (one example is the fourcolour theorem that was proved in 1970s in this way). How do you know the computer works correctly? How do you know the verifier program works correctly? How do you know you encoded the proof requirements and all prerequisites and lemmas correctly?
People have been working on automated proof verification ever since the computer was invented. It is going somewhere, but the validity of such proofs is questionable. You have to accept that a proof can be considered verified by an agent, which encompasses both humans and machines. Machines do not have independent thinking; they are programmed by people, who may and will make errors in the programming. Even if you verify the proof with different machines programmed by different people, they may still all fall prey to the same oversight, and the computers will happily churn the incorrect answer.
Also, the first step in your insufficiency proof is questionable. True, many proofs can be dressed up as linear sequences of statements, expressions, and conditionals, but that's where the analogy ends. More correctly, at the very abstract level a proof is a sequence of transformations from given statements to desired statements. There is no computational state involved, nor any sense of input or output. Rather the prerequisites of the proof are the input and the results the output, and you, the verifier, are the actual program.
Re^6: OT: Mathematics for programming (again) by TGI (Vicar) on Sep 13, 2008 at 02:38 UTC 
Granted, my logic was based on some fast and loose equivalences. Questionable hardly describes it. Isomorphism is not equality, otherwise it would be called equality. I don't have the time or the desire (or perhaps even the ability) to generate a valid, rigorous proof. I was trying to illustrate the thought process which lead me to see the original statement as an outgrowth of, rather than orthogonal to, the CHI.
A perfect system will never happen. Even given a perfect program, perfectly compiled to run on perfect hardware, an imperfect person will provide input and interpret the output. And here we go, Garbage In, Garbage Out. Oops.
But a set of automated tools can help people catch errors. My compilers help me catch errors in my code, and so I am more productive. That's why I use strict and warnings. Those extra picky heuristics catch whole classes of errors for me, and save me endless hours debugging. Any time I spend working on PHP is a strong reminder that a these checks are helpful. A decent, interactive "proof compiler" and an additional "debugger" could be very handy things.
I haven't kept up on my math, but back when I was taking all those credit hours, I found that the best way to screw up a proof (besides beer) was to miss an assumption. The next best way was to fail to see the "right" transformation needed to get things into the "right" shape. Interactive computer assistance could help in the second case, by rapidly sifting a number of potential transformations, until something clicks for the human operator. But there is no guarantee that this will find anything fruitful. I wonder if this kind of tool would serve to enhance the problem with hidden assumptions.
I don't know a cure for the missed assumption. And I'm not sure how to use a computer's strengths to find one. Fortunately there are people who are smarter, better educated, and more dedicated than me working on these things.
Your description of the proof as a system sounds an awful lot like a Turing machine. :) Proofs are recorded in sets of symbols that are systematically manipulated to demonstrate an assertion. (Are proofs completely embodied by these symbolic forms, or is something lost in the ecoding?) As such they should be amenable to automated verification. It seems to me that the problem really lies in a way of creating a proof description language that is flexible and expressive enough to encompass useful research work (not just lame undergraduate homework proofs 'Prove that the infinite series BLAH converges, or diverges'). And yet still structured enough to yield to computation easily.
While I like your metaphor of the mathematician as the program, the system seems to be really a nondeterministic Turing machine. I interpret the corpus of proven statements as the rule set, the current set of symbols embody the state, and the verifier is the lowly head. The proof is really just the trace of the program as the NDTM ran through its paces. A verifier must merely demonstrate that only legal moves were made at each state transition. ( Hmm, this formulation leads me to believe that writing a proof with a computer is equivalent to the halting problem. But don't ask me to prove it. )
Just as I am not the bag of water and assorted chemicals madly fermenting in my chair, I am the process of fermentation, the proof is the process of calculation.
Now I've really wandered off topic. So I'll bring it back on track and summarize. Perfect verification is impossible. We can use our computers to improve our ability to catch a certain (unspecified) set of errors in our mathematical reasoning. The question is, is that set of errors disjoint from the set of errors that we are already good at catching? Or more simply, is automated validation useful?
Thank you for engaging me in this thought provoking discussion.
 [reply] 

( Hmm, this formulation leads me to believe that writing a proof with a computer is equivalent to the halting problem. But don't ask me to prove it. )
I suspect that would be related to the fact that there are statements which are true, but cannot be proven in a formal logic system.
The question is, is that set of errors disjoint from the set of errors that we are already good at catching? Or more simply, is automated validation useful?
A refinement of that last question: what is the cost/benefit ratio of the extra validation? We can be fairly sure that most of the high value / low cost checks have been done already. Syntax checking (highlighting), warnings, strict and taint.
Perfect verification is impossible. We can use our computers to improve our ability to catch a certain (unspecified) set of errors in our mathematical reasoning. This brings to mind another limitation... computers can Do What I Say. Perl's built in flexibility can Do What I Mean, most of the time, when I say things in an unusual way. But there is nothing a computer can do if I do not Say What I Want... Even humans have trouble with that. How do you verify your metacode which tells the verifier what you really wanted to do? Then play the $work game, where what you think is wanted is not exactly what the $customer wants, and what the $customer wants is not exactly what the $customer wants. :)
 [reply] 

