1. 56
  1. 10

    Them: “Leslie Lamport may not be a household name,[…]”

    Me: “The hell he isn’t.” [rage close]

    (I opened it back up and read it anyway. It was actually really interesting. But my rage close was real.)

    1. 17

      There are whole households out there that don’t have a single graduate degree in them. Amazing, I know!

      That said, I didn’t actually know LL was the one behind TLA+, so it was a useful read for me too. (Also, it turns out he actually does look somewhat like the fluffy lion on the cover of the LaTeX book!)

      1. 3

        This is a hypertext book that I intended to be the way to learn TLA+ and PlusCal, until I realized that people don’t read anymore and I made the video course.

        1. 3

          Yeah, I knew he did Lamport clocks but didn’t know he was also the guy who did LaTeX and TLA.

          1. 4

            Inverse for me, I never made the connection between LaTeX Lamport and clock Lamport.

            1. 4

              One did happen before the other.

              1. 10

                Can we really be sure about that.

          2. 3

            I only learned about his writing LaTeX after reading his TLA+ book. Dude doesn’t have much ego, and he only made his name better known when he started actively advocating for formal methods.

          3. 4

            I saw that and ran a Twitter poll

            without googling, can you name one thing Leslie Lamport is known for?

            • yes: 70.1%
            • no: 29.9%

            Not as good as I’d like, but not as bad as the article makes it sound. Granted, this is a heavily skewed demographic. I ran the same poll at work and got 0% yes.

            1. 3

              And even then, people tend to know him more for LaTeX than for his much more important work on distributed computing. Which I’ve heard bothered him.

              1. 5

                I imagine that there are more people writing professional documents than working on distributed computers.

                1. 1

                  On the other hand, I imagine that there are more people using distributed computers than people writing documents. Probably.

                2. 5

                  I can kind of see why that bothered him. Many people viewed TeX as the real, manly typesetting system, and LaTeX was for weaklings. Lamport received the impression of a hippie simplifying Knuth - more an enthusiastic college lecturer than a “real” computer scientist.

                  OTOH LaTeX made TeX usable, and facilitated the distribution of a lot of science. That has to count for something.

                3. 2

                  I know him for Lamport clocks and not much else :)

                  1. 1

                    Heheh. I saw the Twitter poll and thought of this story. I follow you on Twitter now.

                4. 9

                  I have always wanted to write the text on mathematical reasoning for impatient people. I think TLA+ is very interesting, but even some fairly bog-standard case disjunction ideas and “advanced” laws of excluded middle are very powerful.

                  I think the challenge is that people understand these concepts. They understand that something is true or false. But often what is missing is an understanding that what they are looking at is actually a situation where these ideas apply.

                  In a way, it’s like design patterns: people might understand that patterns exist, but the value comes from identifying that the real world problem abstracts to the pattern (or identifying that it doesn’t abstract to it, or abstracts for a subset of cases…).

                  Given how people tend to figure this stuff out from seeing a lot of things in context, I don’t know how you tackle this issue. But I think there’s potential for such a text to instantly make the lives of a lot of more junior engineers much better.

                  1. 3

                    I was working on this a bit last year. It’d just cover classical logic, no combinatorics or graph theory or anything, and devote a lot of space to examples and applications. I think it’d also dip into second order logic- it’s okay for programmers to use a non-absolute framework for reasoning because they’re unlikely to run into the problems that causes.

                  2. 6

                    First I would have to be able to write mathematics with mathematical perfection, I assume.

                    1. 1

                      Mildly amusing:

                      Being beautiful is not something I would say about an algorithm.

                      …and in the video linked from the article:

                      The algorithm still works. […] That is just so beautiful.