5 ms·

If you don't mind me tagging in, TLA+ is a specification language, while Haskell is a programming language. You can choose the granularity of states. So if you

by hwayne 9y ago

If you don't mind me tagging in, TLA+ is a specification language, while Haskell is a programming language. You can choose the granularity of states. So if you were trying to implement a Haskell program that took elements of A and outputted elements of B, in TLA+ you would just say "this all happens in the same state transition." TLA+ isn't, like, a 'better Haskell'. It's more of a 'better UML' or 'a better sack of flowcharts', especially when you are dealing with concurrency. It's an exhaustive checker on the spec. You _can_ use it in the way pron is talking about, but that's not how most people outside academia use it that way.

pron 9y ago
> TLA+ isn't, like, a 'better Haskell'. I dislike the notion of "better" altogether when it comes to software. My point is that FP is not the only nor the most convenient way to reason about software. It has pros and cons, like any other approach; it sometimes very elegant, and sometimes less so. Preference is determined largely by a personal aesthetic preference. I have no qualms whatsoever with those who are more aesthetically drawn to the functional representation of programs. I have a problem with those claiming it is superior to other approaches without any reasonable justification. I am also extremely opposed to claims that people who prefer a non-pure-FP programming language over Haskell do that only because they don't know better. There are very good reasons to prefer either, and they're almost never universal, but depend both on the domain and the team. Also, I'm not comparing TLA+ to Haskell, but rather TLA+ to Lean/Coq, and Eve to Haskell. Synchronous programming languages like Eve (or Esterel/SCADE for realtime systems) are to TLA+ what Haskell is to Lean/Agda (roughly). > You _can_ use it in the way pron is talking about, but that's not how most people outside academia use it that way. I think that you'll find that once you start specifying complex systems (like a distributed database), the refinement relations is extremely useful (in fact, pretty much essential), and is used in practice often (for whatever definition of often is reasonable for formal methods). It makes model-checking (and proofs, but those are rarely used outside academia) much more tractable. I used three levels of refinement, with refinement maps between them, when specifying a distributed database. Refinement is the killer-feature that allows TLA+ to scale. For simple algorithms it is indeed overkill.

by hwayne 9y ago

pron 9y ago

> TLA+ isn't, like, a 'better Haskell'. I dislike the notion of "better" altogether when it comes to software. My point is that FP is not the only nor the most convenient way to reason about software. It has pros and cons, like any other approach; it sometimes very elegant, and sometimes less so. Preference is determined largely by a personal aesthetic preference. I have no qualms whatsoever with those who are more aesthetically drawn to the functional representation of programs. I have a problem with those claiming it is superior to other approaches without any reasonable justification. I am also extremely opposed to claims that people who prefer a non-pure-FP programming language over Haskell do that only because they don't know better. There are very good reasons to prefer either, and they're almost never universal, but depend both on the domain and the team. Also, I'm not comparing TLA+ to Haskell, but rather TLA+ to Lean/Coq, and Eve to Haskell. Synchronous programming languages like Eve (or Esterel/SCADE for realtime systems) are to TLA+ what Haskell is to Lean/Agda (roughly). > You _can_ use it in the way pron is talking about, but that's not how most people outside academia use it that way. I think that you'll find that once you start specifying complex systems (like a distributed database), the refinement relations is extremely useful (in fact, pretty much essential), and is used in practice often (for whatever definition of often is reasonable for formal methods). It makes model-checking (and proofs, but those are rarely used outside academia) much more tractable. I used three levels of refinement, with refinement maps between them, when specifying a distributed database. Refinement is the killer-feature that allows TLA+ to scale. For simple algorithms it is indeed overkill.