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
Return to the
comp.compilers page.
Search the
comp.compilers archives again.