Hacker News Reader

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

View on HN

There's a link to his paper:

http://research.microsoft.com/en-us/um/people/lamport/pubs/p...

Right. It would have been nice to have a short yet more in-depth example in the article.

After 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

[1] Not really surprising. Lamport invented LaTeX.

Reply on news.ycombinator.com