18 Jan 2004 20:53:29 -0500

Related articles |
---|

[8 earlier articles] |

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) |

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

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

Newsgroups: | comp.compilers |

Date: | 18 Jan 2004 20:53:29 -0500 |

Organization: | Oberberg Online Infosysteme |

References: | 03-12-016 03-12-136 04-01-014 04-01-021 04-01-034 04-01-056 04-01-083 |

Keywords: | syntax, theory |

Posted-Date: | 18 Jan 2004 20:53:29 EST |

Hans Aberg wrote:

*> [...]*

I think we've been talking a bit at cross-purpose here:

* You are interested in doing pure mathematics.

* I am interested in proving the properties of programs, with as much

automation as possible and reasonable.

My claims should read in conjunction with my objective; I'm well aware

that they are overgeneral if you want to do general math. This

particularly applies to

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

*>> automatically detectable proofs.*

The main issue here is that, for my objectives, all practically

relevant theorems are those based on a given program. That's a

tremendous amount of information that a theorem prover can use, since

the program structure already reflects the proof structure. Also, all

properties of a program can be proven using constructive

mathematics. This also eases the task of the prover tremendously.

Any theorem prover that's intended for checking (or even finding)

valid theorems in general mathematics has a far harder job: it cannot

restrict itself to constructive mathematics, and it doesn't have a

program. My goals are far more modest than yours :-)

*>> 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.*

*>*

*> Actually, I have a very simple system: One writes the math, axioms,*

*> theorems, proofs, etc., in a file. Then one runs the program, and if*

*> all is syntactically correct, it writes an output file with the same*

*> math, but indicating the statements whose proofs failed. One can get*

*> further diagnostics in a log file, the deductions of selected math*

*> portions, etc. This way, it is usually easy to capture errors.*

This would probably be a good approach for error reporting in a program

property prover as well.

I'm not sure that this is enough though. If the

programmer/mathematician expects the prover to get along from one

theorem to the next without the programmer's help, and the prover

doesn't, this may mean one of two things: Either the prover is too

dumb, or the programmer/mathematician made a mistake. I'm not sure

what strategies would help the programmer/mathematician to find out

which situation holds, and how to remedy the situation in the fastest

possible way.

For programmers, the error may even be in the theorems he wants to

prove (i.e. he stated a theorem that's more general than is needed,

and that actually doesn't hold). I'm not sure how common such a

situation might be for a mathematician (I could imagine that similar

situations could occur when the mathematician sets up a lemma, but I'm

not sure how far this is relevant - the work of a mathematician is far

more open-ended than that of a programmer).

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.