3 ms·
This could have been more precise. The example at the start was great, but there's no example of the lecturer's technique outside of the link to the actual lect
by thejaredhooper 12y ago
This could have been more precise. The example at the start was great, but there's no example of the lecturer's technique outside of the link to the actual lecture
- NSMeta 12y agoThere's a link to his paper: http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/p...
- orbitur 12y agoRight. It would have been nice to have a short yet more in-depth example in the article.
- qznc 12y agoAfter reading that, I think structured proofs should be written with an outliner [0] interface, where you can actually expand and collapse the hierarchy. Lamport also knows this. He repeatedly mentions it as "hypertext". However, he seems to be locked into LaTeX [1] and pdf generation. [0] https://en.wikipedia.org/wiki/Outliner https://en.wikipedia.org/wiki/Outliner [1] Not really surprising. Lamport invented LaTeX.