4 ms·

I remember this from a Leslie Lamport talk posted also on HN a few months ago. Is anyone using this for specifications, prototyping or anything in between in re

by alvatar 11y ago

I remember this from a Leslie Lamport talk posted also on HN a few months ago. Is anyone using this for specifications, prototyping or anything in between in real life?

Twirrim 11y ago
One of my coworkers fleshed out an important and complex component that absolutely had to be logically correct, by using TLA+ modelling. It was the first time he'd used TLA+ (or TLA) at all, and it took a bit of experimenting to get used to it, but he soon generated a solid logical model and exposed a number of fringe flaws in the original proposed solution. From TLA+ model to completed Java application took very little time at all, the logic was all there already, it just needed fleshed out in the language. It was also easy to split the work out amongst multiple programmers. He's argued that the total time, including learning TLA+, took less time than writing the application from scratch in Java and discovering the bugs as they went along. About the only thing he disliked with it was that almost all (if not all) the tooling around it require Eclipse, and he hates that IDE with an almost unholy passion :D
- socceroos 11y ago
  > One of my coworkers fleshed out an important and complex component that absolutely had to be logically correct, by using TLA+ modelling. This is nothing to do with you or your statement, but this is the pre-eminent issue in our industry. Everything absolutely has to be logically correct or we expose users to flaws in both security and stability that can in extreme cases be the difference between life or death and in regular cases be the difference between being cracked or not.
  - nickpsecurity 11y ago
    That's an exaggeration by far: only the tiniest subset of systems can kill people if they fail. Hacks happen by the millions with headaches being the main result along with lost time and money. Even most security-critical systems are the same with the main targeting being done for espionage (data theft). High assurance security focuses on what can get people killed (esp military use) with an emphasis on tools such as these. I've never seen a mainstream FOSS or proprietary product show evidence of an EAL6+ development process, though. Even security community largely throws stuff together plus some code review. Best to keep it real about risks so your solutions match requirements. Most companies are happy to sell patches to broken software or offer software that passed many checklist items for compliance. They have lawyers for the rest.
    - texthompson 11y ago
      Totally agree. Both correctness and security are important, but they're not the only concerns in developing useful software.
    - socceroos 11y ago
      > That's an exaggeration by far: only the tiniest subset of systems can kill people if they fail. Hence calling it an extreme case. > Hacks happen by the millions with headaches being the main result along with lost time and money. ...which is a good reason to make software correct. However, I'm not arguing about the ROI and efficiency of attaining absolute correctness; my point is that software should be correct. Ideally. We're happy to settle for somewhere on the low side of correctness, but I don't think that is necessarily healthy or good for the industry.
      - nickpsecurity 11y ago
        I agree that ideally we should set our baseline much higher. It's why I promote low-defect methodologies, code reviews, static analysis, and languages (eg Ada, Haskell) that prevent/catch most problems early. The few empirical studies done on such things show it actually saves money with occasional productivity boost for one reason: huge reduction of debug time. And the satisfied customer effect can't be ignored. ;)
mulligan 11y ago
At Machine Zone, we've been using formal methods to specify and verify systems we have in development. This is something we've only been doing in the last 6-9 months though.
- ahelwer 11y ago
  Fascinating! I'd love to read a blog post or white paper on this. It does seem like online gaming companies are at the forefront of distributed systems implementation. See League of Legends' use of conflict-free replicated data types, for example: http://highscalability.com/blog/2014/10/13/how-league-of-legends-scaled-chat-to-70-million-players-it-t.html http://highscalability.com/blog/2014/10/13/how-league-of-leg...
- nickpsecurity 11y ago
  By all means, please share it like Amazon did. We need to see and assess every use to both understand and argue their usefulness. Way too few anecdotes from industry.
triggercut 11y ago
http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html http://research.microsoft.com/en-us/um/people/lamport/tla/tl... If anyone is interested and the original article (mentioned elsewhere) as PDF: http://research.microsoft.com/en-us/um/people/lamport/tla/formal-methods-amazon.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/fo...

by alvatar 11y ago

I remember this from a Leslie Lamport talk posted also on HN a few months ago. Is anyone using this for specifications, prototyping or anything in between in real life?

Twirrim 11y ago

One of my coworkers fleshed out an important and complex component that absolutely had to be logically correct, by using TLA+ modelling. It was the first time he'd used TLA+ (or TLA) at all, and it took a bit of experimenting to get used to it, but he soon generated a solid logical model and exposed a number of fringe flaws in the original proposed solution. From TLA+ model to completed Java application took very little time at all, the logic was all there already, it just needed fleshed out in the language. It was also easy to split the work out amongst multiple programmers. He's argued that the total time, including learning TLA+, took less time than writing the application from scratch in Java and discovering the bugs as they went along. About the only thing he disliked with it was that almost all (if not all) the tooling around it require Eclipse, and he hates that IDE with an almost unholy passion :D

socceroos 11y ago
> One of my coworkers fleshed out an important and complex component that absolutely had to be logically correct, by using TLA+ modelling. This is nothing to do with you or your statement, but this is the pre-eminent issue in our industry. Everything absolutely has to be logically correct or we expose users to flaws in both security and stability that can in extreme cases be the difference between life or death and in regular cases be the difference between being cracked or not.
- nickpsecurity 11y ago
  That's an exaggeration by far: only the tiniest subset of systems can kill people if they fail. Hacks happen by the millions with headaches being the main result along with lost time and money. Even most security-critical systems are the same with the main targeting being done for espionage (data theft). High assurance security focuses on what can get people killed (esp military use) with an emphasis on tools such as these. I've never seen a mainstream FOSS or proprietary product show evidence of an EAL6+ development process, though. Even security community largely throws stuff together plus some code review. Best to keep it real about risks so your solutions match requirements. Most companies are happy to sell patches to broken software or offer software that passed many checklist items for compliance. They have lawyers for the rest.
  - texthompson 11y ago
    Totally agree. Both correctness and security are important, but they're not the only concerns in developing useful software.
  - socceroos 11y ago
    > That's an exaggeration by far: only the tiniest subset of systems can kill people if they fail. Hence calling it an extreme case. > Hacks happen by the millions with headaches being the main result along with lost time and money. ...which is a good reason to make software correct. However, I'm not arguing about the ROI and efficiency of attaining absolute correctness; my point is that software should be correct. Ideally. We're happy to settle for somewhere on the low side of correctness, but I don't think that is necessarily healthy or good for the industry.
    - nickpsecurity 11y ago
      I agree that ideally we should set our baseline much higher. It's why I promote low-defect methodologies, code reviews, static analysis, and languages (eg Ada, Haskell) that prevent/catch most problems early. The few empirical studies done on such things show it actually saves money with occasional productivity boost for one reason: huge reduction of debug time. And the satisfied customer effect can't be ignored. ;)

mulligan 11y ago

At Machine Zone, we've been using formal methods to specify and verify systems we have in development. This is something we've only been doing in the last 6-9 months though.

ahelwer 11y ago
Fascinating! I'd love to read a blog post or white paper on this. It does seem like online gaming companies are at the forefront of distributed systems implementation. See League of Legends' use of conflict-free replicated data types, for example: http://highscalability.com/blog/2014/10/13/how-league-of-legends-scaled-chat-to-70-million-players-it-t.html http://highscalability.com/blog/2014/10/13/how-league-of-leg...
nickpsecurity 11y ago
By all means, please share it like Amazon did. We need to see and assess every use to both understand and argue their usefulness. Way too few anecdotes from industry.

triggercut 11y ago

http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html http://research.microsoft.com/en-us/um/people/lamport/tla/tl... If anyone is interested and the original article (mentioned elsewhere) as PDF: http://research.microsoft.com/en-us/um/people/lamport/tla/formal-methods-amazon.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/fo...