5 ms·

Leslie Lamport (of Paxos, LaTeX, and TLA+ fame) has been making this point for years. Basically that in order to design a piece of software, you need to be able

Leslie Lamport (of Paxos, LaTeX, and TLA+ fame) has been making this point for years. Basically that in order to design a piece of software, you need to be able to create a spec, and the best way of doing that is through mathematics. E.g. - https://lamport.azurewebsites.net/tla/math-knowledge.html https://lamport.azurewebsites.net/tla/math-knowledge.html - https://youtu.be/-4Yp3j_jk8Q https://youtu.be/-4Yp3j_jk8Q

pmiller2 7y ago
I agree in principle, but there’s a rather fundamental problem here: writing the spec has to be easier than writing the program. Otherwise,we should just write a compiler for the spec language and save ourselves a step, or blunder on by writing the program without a spec, as is usually done.
- anaphor 7y ago
  I think if you're doing your spec as a combination of high level set theory or algebra and some prose, then it should be easier than writing the program itself (assuming you know a bit about math and how to write a spec). The question is how much time is it worth putting into writing a detailed spec. I think the answer is that it really depends on the size and complexity of your software. I think the idea is that programmers have to be comfortable with writing something down, even if it's not perfect. A half-baked spec is better than no spec, basically. Otherwise you will likely end up with spaghetti code that needs to be rewritten or scrapped.
  - pmiller2 7y ago
    I already write my specs as a combination of math and prose. It’s just that the math portion is empty. /s Seriously, though, that prose portion is where the vast majority of the bugs will be.
- AlexCoventry 7y ago
  Writing a useful TLA+ spec will usually be easier than writing an operational program with the functionality the spec describes, because it lets you abstract over the uninteresting parts.
  - pmiller2 7y ago
    That seems like it just pushes all the bugs into the “uninteresting” parts.
    - AlexCoventry 7y ago
      Not really. Some parts are harder to reason about than others, especially interactions between components of a distributed system.
    - hwayne 7y ago
      It pushes the bugs to things that are easier to test. You write tests for things like "we properly error on a malformed input" and write TLA+ specs for things like "there are no awful concurrency bugs spanning three servers in two regions."

pmiller2 7y ago

I agree in principle, but there’s a rather fundamental problem here: writing the spec has to be easier than writing the program. Otherwise,we should just write a compiler for the spec language and save ourselves a step, or blunder on by writing the program without a spec, as is usually done.

anaphor 7y ago
I think if you're doing your spec as a combination of high level set theory or algebra and some prose, then it should be easier than writing the program itself (assuming you know a bit about math and how to write a spec). The question is how much time is it worth putting into writing a detailed spec. I think the answer is that it really depends on the size and complexity of your software. I think the idea is that programmers have to be comfortable with writing something down, even if it's not perfect. A half-baked spec is better than no spec, basically. Otherwise you will likely end up with spaghetti code that needs to be rewritten or scrapped.
- pmiller2 7y ago
  I already write my specs as a combination of math and prose. It’s just that the math portion is empty. /s Seriously, though, that prose portion is where the vast majority of the bugs will be.
AlexCoventry 7y ago
Writing a useful TLA+ spec will usually be easier than writing an operational program with the functionality the spec describes, because it lets you abstract over the uninteresting parts.
- pmiller2 7y ago
  That seems like it just pushes all the bugs into the “uninteresting” parts.
  - AlexCoventry 7y ago
    Not really. Some parts are harder to reason about than others, especially interactions between components of a distributed system.
  - hwayne 7y ago
    It pushes the bugs to things that are easier to test. You write tests for things like "we properly error on a malformed input" and write TLA+ specs for things like "there are no awful concurrency bugs spanning three servers in two regions."