5 ms·

> It is 100% false that a semantic domain of partial functions makes your state space in any way smaller than if your semantics domain is sets of behaviors. It'

by tome 9y ago

> It is 100% false that a semantic domain of partial functions makes your state space in any way smaller than if your semantics domain is sets of behaviors. It's just not true. Of course it's true. There's a surjection from behivours to partial functions. Proving things about denotational semantics is obviously easier than proving things about operational semantics. It's just less useful. > > I can't believe that state-based reasoning could ever displace expression-based reasoning, since (as seen in your own talk examples) even very short expressions can correspond to absolutely enormous spaces of possible states. > This is just mathematically wrong, because if you think of the cardinality of functions you'd realize that it's the same as (normally bigger, actually) than that of sequences (e.g. the set of functions from the natural numbers to the natural numbers is exactly that of sequences of natural numbers). I think you must have misunderstood. Here's a simple example. There are finitely many partial functions between finite sets A and B but infinitely many sequences of state transitions that take states in A to states in B.

pron 9y ago
> Of course it's true. There's a surjection from behivours to partial functions. No, it is false. If all your functions were on simple types, then you would be correct (although the cardinality is still the same), but in order to express some programs using function semantics, you need to have higher-order functions, which vastly increase your state space. > Proving things about denotational semantics is obviously easier than proving things about operational semantics. It's just less useful. Again, what operational and denotational semantics are depends entirely on the formalism. The operational semantics of TLA don't even express the computation at all. > There are finitely many partial functions between finite sets A and B but infinitely many sequences of state transitions that take states in A to states in B. But the sequences exist in a lattice! I'm being very imprecise (to say the least; this is actually wrong, but conveys the idea) here, but just to give you an intuition, the sequence <1, 5, 6, 7, 8, 12, 0, 2, 1, 8, 6> is "smaller" in the lattice than the sequence <1, 6>. If your proposition is true for the latter, it is automatically true for the former. You never work with all possible sequences. In fact, there are infinite levels of them. Between any two states in a TLA+ behavior, there is an unbounded (yet finite) number of other states that are implicitly ignored. So what? The "state space" of which you reason is exactly the same as that of a "function" (assuming the function has enough information to prove the proposition, i.e., that it's not about complexity etc.). > Be careful to pay attention to what lmm actually claimed. The claim was about "proof of properties of program fragments ... in "normal" industrial code ... ordinary webapps". AFAIK, the only industrial grade, web programs etc., for which formal methods are used are Amazons AWS and some of Oracle's web services, that use TLA+. Whether or not someone uses Haskell, Haskell simply falls too short of "formal methods". > Any language is referentially transparent if every expression is only denotationally equal to itself. No, that's just not true. The only way that would work is if your denotation is the syntax itself, and that's just not what people mean when they talk about semantics in general. Template Haskell and Lisp are not referentially transparent. Regardless of what the denotation of term a is, you cannot replace it with any term b having the same denotation (and one exists unless your "denotation" is the syntax) while preserving the denotation of the complete expression. > claiming the Java is referentially transparent is almost vacuous. Except that the person who claimed it was Christopher Strachey in a seminal paper of programming language theory. No, it is not vacuous in the least. > From there we conclude that Haskell's is more useful. I know you very strongly believe that (and I do not), but there's neither the theoretical justification nor the empirical evidence (at least so far) to support that. From the fact that you can assign simple and clear semantics to some kinds of computation you most certainly cannot conclude that the formalism is more useful in general. It all comes down to aesthetics and pragmatics. You like Haskell better than Java (and I like Java better than Haskell), and you are more productive in Haskell than Java (and I'm more productive in Java). That's all. Unless we have evidence of either being universally more productive than the other, we simply cannot make such claims. And that's OK! You can evangelize Haskell showing people what you like about it and why you think it's great. I just don't like these sweeping claims that have no justification. This applies to everything, BTW, even to Scheme, ML, Java and TLA+ -- all of which I really like. I can rarely if ever bring myself to believe that some approach to software is universally (or close to it) better than others, unless there is some very compelling evidence. > Do you know the precise time in the video? No. I remember Leroy mentioning it at the very beginning, and then they discuss it at some later point, as well.
- tome 9y ago
  It's obvious you're not making even the most cursory effort to understand the claims of your interlocutors. The info you have provided about TLA+ is extremely useful and I hope you can see that I have made a good faith effort to understand your point of view. However, I do not feel an equal effort back towards my position, so I'm afraid I'll have to leave it there.
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 tome 9y ago

pron 9y ago

> Of course it's true. There's a surjection from behivours to partial functions. No, it is false. If all your functions were on simple types, then you would be correct (although the cardinality is still the same), but in order to express some programs using function semantics, you need to have higher-order functions, which vastly increase your state space. > Proving things about denotational semantics is obviously easier than proving things about operational semantics. It's just less useful. Again, what operational and denotational semantics are depends entirely on the formalism. The operational semantics of TLA don't even express the computation at all. > There are finitely many partial functions between finite sets A and B but infinitely many sequences of state transitions that take states in A to states in B. But the sequences exist in a lattice! I'm being very imprecise (to say the least; this is actually wrong, but conveys the idea) here, but just to give you an intuition, the sequence <1, 5, 6, 7, 8, 12, 0, 2, 1, 8, 6> is "smaller" in the lattice than the sequence <1, 6>. If your proposition is true for the latter, it is automatically true for the former. You never work with all possible sequences. In fact, there are infinite levels of them. Between any two states in a TLA+ behavior, there is an unbounded (yet finite) number of other states that are implicitly ignored. So what? The "state space" of which you reason is exactly the same as that of a "function" (assuming the function has enough information to prove the proposition, i.e., that it's not about complexity etc.). > Be careful to pay attention to what lmm actually claimed. The claim was about "proof of properties of program fragments ... in "normal" industrial code ... ordinary webapps". AFAIK, the only industrial grade, web programs etc., for which formal methods are used are Amazons AWS and some of Oracle's web services, that use TLA+. Whether or not someone uses Haskell, Haskell simply falls too short of "formal methods". > Any language is referentially transparent if every expression is only denotationally equal to itself. No, that's just not true. The only way that would work is if your denotation is the syntax itself, and that's just not what people mean when they talk about semantics in general. Template Haskell and Lisp are not referentially transparent. Regardless of what the denotation of term a is, you cannot replace it with any term b having the same denotation (and one exists unless your "denotation" is the syntax) while preserving the denotation of the complete expression. > claiming the Java is referentially transparent is almost vacuous. Except that the person who claimed it was Christopher Strachey in a seminal paper of programming language theory. No, it is not vacuous in the least. > From there we conclude that Haskell's is more useful. I know you very strongly believe that (and I do not), but there's neither the theoretical justification nor the empirical evidence (at least so far) to support that. From the fact that you can assign simple and clear semantics to some kinds of computation you most certainly cannot conclude that the formalism is more useful in general. It all comes down to aesthetics and pragmatics. You like Haskell better than Java (and I like Java better than Haskell), and you are more productive in Haskell than Java (and I'm more productive in Java). That's all. Unless we have evidence of either being universally more productive than the other, we simply cannot make such claims. And that's OK! You can evangelize Haskell showing people what you like about it and why you think it's great. I just don't like these sweeping claims that have no justification. This applies to everything, BTW, even to Scheme, ML, Java and TLA+ -- all of which I really like. I can rarely if ever bring myself to believe that some approach to software is universally (or close to it) better than others, unless there is some very compelling evidence. > Do you know the precise time in the video? No. I remember Leroy mentioning it at the very beginning, and then they discuss it at some later point, as well.

tome 9y ago
It's obvious you're not making even the most cursory effort to understand the claims of your interlocutors. The info you have provided about TLA+ is extremely useful and I hope you can see that I have made a good faith effort to understand your point of view. However, I do not feel an equal effort back towards my position, so I'm afraid I'll have to leave it there.

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.