http://www.perlmonks.org?node_id=710499


in reply to Re^2: OT: Mathematics for programming (again)
in thread OT: Mathematics for programming (again)

That isomorphism is interesting, but orthogonal to what I was trying to say. I would say that your point is part of the reason why there is such a good parallel between doing mathematics and writing programs. However the point that I was trying to make is that our customary way of doing mathematics is like programming where you only outline the program. You don't write it out completely, you don't run it through a compiler, you don't do QA on it. You just do desk checking on a program that has never actually been written and convince yourself that it would work.

If I wanted to draw a parallel to a famous quote, I would go with Knuth's, Beware of bugs in the above code; I have only proved it correct, not tried it.

Replies are listed 'Best First'.
Re^4: OT: Mathematics for programming (again)
by TGI (Parson) on Sep 11, 2008 at 17:50 UTC

    I don't know that they are orthogonal, one follows from the other. Here's the logic as I see it:

    1. A proof is a program.
    2. A mentally validated proof is a mentally validated program.
    3. Mental validation is insufficient to verify programs are correct.
    4. Therefore mental validation is insufficient to verify proofs are correct.

    There's all kinds of work in formal methods for creating provably correct programs. It seems like you are calling for the converse: computer verifiable proofs.

    I'n not sure how you'd do this, but I think you'd need to have some notational system that encompasses all of mathematics to start. Where are Russell and Whitehead when you need them? :)

    Automated verification of proofs is such a good idea that it looks like people are working on this now.

    Your argument for automated verification of proofs is persuasive. Thanks for bringing the idea up, it has provided me with some interesting things to think about while procrastinating.


    TGI says moo

      Alright, say you program a computer to verify a hairy proof (one example is the four-colour 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.

      --
      print "Just Another Perl Adept\n";

        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 non-deterministic 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.


        TGI says moo