Beefy Boxes and Bandwidth Generously Provided by pair Networks
Perl: the Markov chain saw
 
PerlMonks  

Re^6: OT: Mathematics for programming (again)

by TGI (Parson)
on Sep 13, 2008 at 02:38 UTC ( [id://711048]=note: print w/replies, xml ) Need Help??


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

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

Replies are listed 'Best First'.
Re^7: OT: Mathematics for programming (again)
by SuicideJunkie (Vicar) on Sep 16, 2008 at 12:38 UTC
    ( 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 meta-code 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. :)

Log In?
Username:
Password:

What's my password?
Create A New User
Domain Nodelet?
Node Status?
node history
Node Type: note [id://711048]
help
Chatterbox?
and the web crawler heard nothing...

How do I use this?Last hourOther CB clients
Other Users?
Others chilling in the Monastery: (2)
As of 2024-03-19 05:23 GMT
Sections?
Information?
Find Nodes?
Leftovers?
    Voting Booth?

    No recent polls found