26 Nov 2005 00:17:53 -0500

From: | henry@spsystems.net (Henry Spencer) |

Newsgroups: | comp.compilers |

Date: | 26 Nov 2005 00:17:53 -0500 |

Organization: | SP Systems, Toronto, Canada |

References: | 05-10-053 05-11-004 05-11-014 05-11-028 |

Keywords: | syntax, design |

Posted-Date: | 26 Nov 2005 00:17:53 EST |

Hans Aberg <haberg@math.su.se> wrote:

*>[human-readable theorem-prover output]*

*>In addition, I have recently started to use Unicode UTF-8, using correct*

*>mathematical symbols instead of ASCII words. This turns out to help up the*

*>code a great deal.*

You might also want to have a look at Lamport's paper "How to write a

long formula" (DEC SRC-119, 1994), possibly still findable at

<http://gatekeeper.dec.com/pub/DEC/SRC/research-reports/SRC-119.pdf>,

in which he relates some experience with notations for presenting

lengthy program-correctness formulas.

--

spsystems.net is temporarily off the air; | Henry Spencer

mail to henry at zoo.utoronto.ca instead. | henry@spsystems.net

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.