4 ms·

geoftt isn’t asking whether metaphorical TLA+ is academically fruitful. He’s asking if Amazons et al. have _continued_ to use it, and whether there’s some volum

geoftt isn’t asking whether metaphorical TLA+ is academically fruitful. He’s asking if Amazons et al. have _continued_ to use it, and whether there’s some volume of evidence attesting to this.

streetcat1 7y ago
Sure. So if amazon did not continue to use it. Does TLA+ suddenly become not useful? My point here is that those tools are theoretical CS tools based on the underlying nature of computers - which are a discrete digital state machine. Why do you even use high level languages, why not just program in assembler?
- traderjane 7y ago
  If the Amazons of the world tried and dropped TLA+, that is signal to people who were on edge of technological adoption. If we received data on its efficacy during its trials, we'd be even more informed, as people are interested in more than the internal consistency of a system. Right now some people have a theory that Uncle Bob is noise in the sea of architectural opinion, and we can't move forward because we don't have enough data. The call for more data is welcome by me.
  - spenczar5 7y ago
    Amazon continues to use TLA+. I work there. It's not a tool needed every day, and it's not needed by everyone (really, not by almost _anyone_). But sometimes it's the best tool for the job. You won't be getting much data on this because companies are secretive. The way it's used is to ensure correctness of distributed systems. A classic example might be ensuring that a model for backing up customer data is unable to get into indeterminate state. It's important to get the model right. But the model isn't code - TLA is not a programming language, it's a tool for modeling state machines; yes, of course, one needs to also write software to deliver value.
- geofft 7y ago
  > Sure. So if amazon did not continue to use it. Does TLA+ suddenly become not useful? Yes. (Or more precisely, it never was useful.) Zero part of my business requirements involve anything about discrete digital state machines. If I could deliver business value more efficiently with pen and paper, I would. If I could deliver business value more efficiently with Excel or a shell one-liner, I would (and do). If I could deliver business value more efficiently by singing my harmony into the Music of the Ainur, I would. I write software because it's the tool we've found that is most efficient at delivering business value, not because the software itself has value. So I use high-level languages because they are demonstrably more efficient. (And I frequently write sloppy code in Python or awk because it helps me answer business-relevant questions like "why is the site slow" quickly, without demanding I be rigorous about my software engineering in the process of answering the question.) don't use UML because I have yet to see evidence that it will help me deliver business value more effectively. (I do also enjoy writing software as a practice, and I do that on weekends. That's the time to make code for code's sake.)

geoftt isn’t asking whether metaphorical TLA+ is academically fruitful. He’s asking if Amazons et al. have _continued_ to use it, and whether there’s some volume of evidence attesting to this.

streetcat1 7y ago

Sure. So if amazon did not continue to use it. Does TLA+ suddenly become not useful? My point here is that those tools are theoretical CS tools based on the underlying nature of computers - which are a discrete digital state machine. Why do you even use high level languages, why not just program in assembler?

traderjane 7y ago
If the Amazons of the world tried and dropped TLA+, that is signal to people who were on edge of technological adoption. If we received data on its efficacy during its trials, we'd be even more informed, as people are interested in more than the internal consistency of a system. Right now some people have a theory that Uncle Bob is noise in the sea of architectural opinion, and we can't move forward because we don't have enough data. The call for more data is welcome by me.
- spenczar5 7y ago
  Amazon continues to use TLA+. I work there. It's not a tool needed every day, and it's not needed by everyone (really, not by almost _anyone_). But sometimes it's the best tool for the job. You won't be getting much data on this because companies are secretive. The way it's used is to ensure correctness of distributed systems. A classic example might be ensuring that a model for backing up customer data is unable to get into indeterminate state. It's important to get the model right. But the model isn't code - TLA is not a programming language, it's a tool for modeling state machines; yes, of course, one needs to also write software to deliver value.
geofft 7y ago
> Sure. So if amazon did not continue to use it. Does TLA+ suddenly become not useful? Yes. (Or more precisely, it never was useful.) Zero part of my business requirements involve anything about discrete digital state machines. If I could deliver business value more efficiently with pen and paper, I would. If I could deliver business value more efficiently with Excel or a shell one-liner, I would (and do). If I could deliver business value more efficiently by singing my harmony into the Music of the Ainur, I would. I write software because it's the tool we've found that is most efficient at delivering business value, not because the software itself has value. So I use high-level languages because they are demonstrably more efficient. (And I frequently write sloppy code in Python or awk because it helps me answer business-relevant questions like "why is the site slow" quickly, without demanding I be rigorous about my software engineering in the process of answering the question.) don't use UML because I have yet to see evidence that it will help me deliver business value more effectively. (I do also enjoy writing software as a practice, and I do that on weekends. That's the time to make code for code's sake.)