12 Jan 2004 13:24:57 -0500

Related articles |
---|

[6 earlier articles] |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2003-12-21) |

Re: Layout syntax haberg@matematik.su.se (2003-12-23) |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2003-12-27) |

Re: Layout syntax haberg@matematik.su.se (2004-01-02) |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2004-01-07) |

Re: Layout syntax haberg@matematik.su.se (2004-01-09) |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2004-01-12) |

Re: Layout syntax haberg@matematik.su.se (2004-01-16) |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2004-01-18) |

Re: Layout syntax bayard@newsguy.com (Ian Zimmerman) (2004-01-18) |

Re: Layout syntax haberg@matematik.su.se (2004-01-22) |

Re: Layout syntax haberg@matematik.su.se (2004-01-22) |

Re: Layout syntax bayard@newsguy.com (Ian Zimmerman) (2004-02-01) |

[1 later articles] |

From: | Joachim Durchholz <joachim.durchholz@web.de> |

Newsgroups: | comp.compilers |

Date: | 12 Jan 2004 13:24:57 -0500 |

Organization: | Oberberg Online Infosysteme |

References: | 03-12-016 03-12-060 03-12-081 03-12-104 03-12-112 03-12-124 03-12-131 03-12-136 04-01-014 04-01-021 04-01-034 |

Keywords: | syntax, theory |

Posted-Date: | 12 Jan 2004 13:24:57 EST |

Hans Aberg wrote:

*> So when merely attempting to implement a proof checker for formal*

*> proofs written out in full that makes a correct use of*

*> metamathematics, there are a number of mathematical subtleties,*

*> which I do not think any system today handles. Surprise, surprise!*

Interesting - I had been thinking that this kind of thing was long solved.

*> -- But if somebody can give me a reference to a 100% correct proof*

*> checking system according to standard metamathematics, please let me*

*> know.*

Coq? At least that's what's usually quoted at this point of the

discussion (but I don't know much about it myself).

*> Then, if one by a proof means what humans usually write, then there*

*> is no clear distinction between a proof checker and a theorem prover,*

*> as the human written simplified proof merely invokes a proof search*

*> engine that is doing more work. The most extremely simplified proof*

*> is the empty one, which leads to the classical idea of a theorem*

*> prover. Also, the search engine will in any case be a modified Prolog*

*> type proof engine, so from the point of implementation, there is no*

*> clear distinction either.*

At a minimum, the hand-written proof must include the sub-theorems of

all proofs by induction that are needed (and such a proof is required

for every loop and every recursion present, and the induction

information translates to loop invariants resp. assertions on the

recursive functions).

And, of course, the final theorems that one wants proven should be

written down :-)

These are the minimum requirements to make the task of giving a proof

decidable. Besides, explicitly writing down loop invariants will improve

code readability, so it's no loss if programmers have to write this down.

After that, constructing the proof is "just" worst-case exponential in

time and space... but there are a few theorems in Formal Logic that can

drastically cut down the search space.

*> Also, not every theorem has a proof (by Goedel incompleteness), and*

*> there is no algorithm to tell which theorems have a proof.*

It's my firm belief that all practically relevant theorems have

automatically detectable proofs.

There may be algorithms that are difficult to prove. However, these are

usually written with lots of explanations *how* the algorithm works -

which is an informal precursor to the full proof. Actually, the more

difficult algorithms are more rigorously proven, so I'd expect that

theorem provers will get more help for the more difficult software,

simply because humans need more help as well.

BTW when looking at the source code of a typical program, the required

"proofs" aren't much more than modus ponens, with the occasional

transformation of boolean expressions. That's no wonder: other

programming styles tend to be unmaintainable.

*>> I meant checking that the theorem being proven is actually what we*

*>> want proven.*

*>*

*> The way you have worded this sentence, there is no way for a computer*

*> to tell if a theorem makes sense; only humans can do that.*

Exactly.

The computer is *never* able to determine whether something makes sense

(read: is what we humans want).

My idea of theorem proving in connection with practical programming goes

like this:

1. The programmer writes a program.

2. The programmer wants to make sure that his program satisfies some

property. The exact nature of that property can vary: it might be a

statement on the program's results (or just a part of its results), or

on resource usage, or that it doesn't access certain resources, or

doesn't leak information - whatever the situation, it's the programmer

who decides which properties are interesting in the first place.

3. The programmer formalizes the properties, getting a theorem.

4. The theorem prover proves (or disproves) the theorem.

Of course, details may vary wildly. The theorems could be set up before

the first line of code is written. The programmer might have to state

lemmas to help the theorem prover along. The theorem prover would have

to be quite smart about reporting errors, since just a "the property

doesn't hold" response isn't going to be very helpful. Etc. etc.

But I think that it could be done, with current technology. Even if

there's no working theorem prover that correctly handles all current

metamathematics - we don't need to prove mathematical statements, we

want to prove statements about programs, at the level of formalization

that the relevant programming language has. We can even tell the theorem

prover to ignore the murky corners of the language definition ("assuming

that the following computation doesn't throw an exception, the result

will not be larger than twice the input" might be an theorem of that

kind - it's not as general as one would like, but it would be better

than nothing, right?)

*>> For example, every tax calculation program is an existence proof*

*>> for a best way of filling out the tax forms given a set of input*

*>> parameters under the constraints of obeying the tax laws. This can*

*>> also be done in reverse: when I have a proof that such a solution*

*>> exists, without using the law of the excluded middle, then a*

*>> program that calculates the value can be automatically derived from*

*>> the proof.*

*>*

*> What you describe here is just a standard way to form a mathematical*

*> theory: One has as a basis certain axioms and rules of inference*

*> (essentially Prolog clause plus metamathematical typing), and proves*

*> from them some theorems. Then from axioms and theorems, one may want*

*> to prove new theorems.*

*>*

*> When one calculates a value, invokes a proved algorithm, or proves*

*> that two an implementation of an algorithm actually produces the*

*> results of the algorithm, those are just examples of theorems with*

*> proof. So, from the formal point of view, one does not get anything*

*> new here, even though it may be difficult to find good ways to*

*> implement practical systems.*

Exactly my point.

*> Eventually, I embarked onto the idea of attempting to implement a*

*> formally correct metamathematics. I use books on metamathematics by*

*> Elliott Mendelson, Stephen Cole Kleene, and Joseph R. Shoenfield. On*

*> that road I am right now.*

This sounds interesting in its own right.

Regards,

Jo

--

Currently looking for a new job.

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.