Re:Kotlin: A Language with a Bright Future
by pron on Wednesday November 29, 2017 @03:38PM
(#15810615)
> 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.
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.