7 Jan 2004 00:56:38 -0500

Related articles |
---|

[4 earlier articles] |

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

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

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

[3 later articles] |

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

Newsgroups: | comp.compilers |

Date: | 7 Jan 2004 00:56:38 -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 |

Keywords: | syntax |

Posted-Date: | 07 Jan 2004 00:56:38 EST |

Hans Aberg wrote:

*> <joachim.durchholz@web.de> wrote:*

*>>After all, proofs aren't just read by computers, they are also read by*

*>>humans (e.g. to check whether a proof states what was intended, or to*

*>>modify a proof to prove something slightly different but more*

*>>interesting), and humans don't parse nested constructs very well.*

*>*

*> So it will not be needed to wrote proofs so that*

*> humans can directly check them, even though humans still must be able*

*> to write proofs.*

I didn't mean checking the validity of the proof - programs for doing

that have been written decades ago.

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

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

When I mistype or misinterpret the laws, the program is still a proof

(resp. there's still a specification and an automatically deduced

program), but not for the theorem that I wanted proven.

*>>I think we're largely in agreement, and just differ in how far one*

*>>should go when trying to import mathematical conventions into a*

*>>computerized language.*

*>*

*> Let's generalize typical computer type systems, and see where we might*

*> land: Hindley-Milner type systems rely on unification to resolve*

*> polymorphic types. The next generalization might be a type system that*

*> make use of a Prolog engine, of which unification is a part then. And*

*> generalizing that, one might instead make use of a proof checking*

*> engine, based on metamathematics. Then the type system might be*

*> something like axiomatic set theory. If one gets that far, one has*

*> unified computer type systems with pure math. :-)*

Actually that's a road that I'd like to explore. (I think it's already

being done in academia, though I haven't heard of practial results yet.)

Regards,

Jo

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.