I feel like a lot of Meyer’s stuff follows a pattern: he denigrates other people’s approaches to problems because they’re not his approach, and his approach is best by the virtue of being his approach. One example from this paper:
Consider first Gilles Kahn’s classic “Natural Semantics” paper [19]. It specifies a simple programming lan-
guage and has a list of definitions for programming constructs, assuming a considerable mathematical baggage.
The semantics of the conditional expression (“if … then … else …”), for example, is specified through two
inference rules: [cut]
One can only shake one’s head: the notion of conditional expression can be explained in full to a 6-year-old: wherever E1 holds use E2 , otherwise use E3 . You may summon Fig. 4 for help.
Meyer mocks natural semantics without ever explaining the actual point of it: as a basis for tooling. Sure, conditional expression is intuitive to a 6-year-old, but I can’t force a 6-year-old inside my type checker!
This is especially ironic, because here’s Meyer’s later definition of the “conditional expression” if C then p else q:
if C then p else q end
->
if C: p, C’: q end
->
(C: p) ∪ (C': q)
->
<post_p / C, Pre_p ∩ C> ∪ <post_q / C', Pre_q ∩ C'>
->
<⌊post_p / C⌋ ∪ ⌊post_q / C'⌋ , (Pre_p ∩ C) ∪ (Pre_q ∩ C')>
Where C’ = “the complement of C” (not defined, but later indicated to be “¬C”), ⌊p⌋ = “Rounded version of p” ⟨post_p / Pre_p, Pre_p⟩, r / X is the set {[x, y] ∈ R | x ∈ X]. I’m not fully clear on what it means to “round” a postcondition; he only defines “rounding” a whole program.
Now compare this to what was so bad one could only “shake one’s head”:
but yeah, rounding is defined in the article only for programs, not for postconditions.
I’m skeptical about what this article contributes to the field (has this really not been done before?), but I could believe that building a theory of computation directly on set theory would be convenient for reusing set theory ideas and tools in computation theory.
This is simple vs. easy. It definitely is very simple mathematics, pretty basic set theory (not Venn diagram basic, as it needs functions&relations, but nothing even remotely crazy). It probably isn’t easy for most people, as I think this “foundations of mathematics” stuff is not frequently taught, and it does require somewhat more abstract thinking.
Perhaps even the question itself is a type error.
Sure, programming is mostly done via Turing-complete languages, and a Turing-completeness is surprisingly easy/trivial to reach. (Doesn’t make “the sum of its parts” any easier though, two trivial function’s composition may not end up as a trivial function.)
As for why I consider it a type error: programming is the whole act and art of building and maintaining computable functions with certain properties, if we want to be very abstract.
Naming variables, encoding business logic/constraints in a safe way, focusing on efficiency are all parts of programming itself. The computing model is just one (small) part of it all.
The computing model is just one (small) part of it all.
Related:
“(Alan) Turing’s work is very important; there is no question about that. He illuminated many fundamental questions. In a sense, however, it is unfortunate that he chose to write in terms of ‘computability’ especially in view of development, subsequent to Turing’s work, of modern computers. As a theory of ‘computability’, Turing’s work is quite important, as a theory of ‘computations’, it is worthless.
No mention at all of TLA+ in the paper? TLA+ has no known axioms it relies on to my knowledge. It’s also just “simple math”, i.e. set theory and predicate logic. I didn’t see anything that was all that different from TLA+ here, except TLA+ talks way more about actual program execution, which I didn’t see that much of here.
I mean I like the idea, for the same reason that I like TLA+: it’s actually digestible. Set theory really is simple and understandable, vs. something like dependent type theory.
I just didn’t understand some of the criticisms, for example how is this definition of refinement different than any others? It seems like the same thing.
I think TLA⁺ does have axioms, since it has to define what the temporal logic of actions is. So in A Science of Concurrent Programs Lamport goes through simpler constructions like the “Logic of Actions” which introduces sequences of states indexed by a time parameter, then on to “Raw Temporal Logic of Actions” which gets rid of the time parameter and defines the □ operator, finally ending up at the “Temporal Logic of Actions” which requires formulas to be stuttering-insensitive so introduces □[A]ᵥ and ◇⟨A⟩ᵥ. It all ultimately is built on top of the Kahn model mentioned in this paper where variables are mapped to specific values in a given state.
Lamport also cautions that TLA is weirder than ordinary predicate logic on page 69 of A Science of Concurrent Programs:
Although elegant and useful, temporal logic is weird. It’s not ordinary math. In ordinary math, any operator Op we can define satisfies the condition, sometimes called substitutivity, that the value of an expression Op(e1, . . . , en ) is unchanged if we replace any ei by an expression equal to ei. […] However, the temporal operator □ is not substitutive.
You’re right TLA⁺ does have a simple definition of refinement, where a system described by TLA formula P refines a system described by TLA formula Q if P ⇒ Q. However, this isn’t really unique; actually Exercise 9 of Chapter 1.1 (Volume 1) of The Art of Computer Programming has you invent a set-theoretic definition of refinement whole-cloth (it’s a fun exercise, take a look at it!).
yea, I was mistaken, TLA does have axioms (figure 5 in section 5.6 in Temporal Logic of Actions).
I’ll check out that exercise at some point. I’m in the “refinement is one of the most important ideas in CS” camp, so any deeper insight there is always welcome.
I am aware of some limitations of refinement, for example a program which does nothing (has no observable behaviors) refines every program vacuously. But this is just a consequence of refinement being defined in terms of subset / implication: the empty set is a subset of everything, false implies true, etc.
But I didn’t see how these refinement definitions had any benefit so far.
The vacuous refinement case is annoying because it’s definitely possible to accidentally write an inconsistent fairness constraint ensuring your program generates zero behaviors, thus vacuously satisfying any refinement relation you’re trying to check. I proposed adding a warning if this happens: https://github.com/tlaplus/tlaplus/issues/161
The approaches «relying» on large sets of axioms and/or reasoning rules often come with models and pretty easy soundness proofs. Consistency/nontriviality is not as much of an issue as claimed.
The reason to go with weirdly carved axioms despite having a model is to have proof tools (sometimes in the sense of lemmas, sometimes in the sense of software) suitable for everything that is expressible at all. Arbitrary set theory claims are sometimes needed but don’t make proof tools easy…
I feel like a lot of Meyer’s stuff follows a pattern: he denigrates other people’s approaches to problems because they’re not his approach, and his approach is best by the virtue of being his approach. One example from this paper:
Meyer mocks natural semantics without ever explaining the actual point of it: as a basis for tooling. Sure, conditional expression is intuitive to a 6-year-old, but I can’t force a 6-year-old inside my type checker!
This is especially ironic, because here’s Meyer’s later definition of the “conditional expression”
if C then p else q:Where C’ = “the complement of C” (not defined, but later indicated to be “¬C”), ⌊p⌋ = “Rounded version of p” ⟨post_p / Pre_p, Pre_p⟩,
r / Xis the set{[x, y] ∈ R | x ∈ X]. I’m not fully clear on what it means to “round” a postcondition; he only defines “rounding” a whole program.Now compare this to what was so bad one could only “shake one’s head”:
Which is easier to understand? Which is easier to programmatically evaluate?
To be fair, we’ve had lots of training and years to grok the Kahn notation, and 12 hours to digest the Meyer one.
This is at least a very authentic Meyer paper, we can be pretty sure it’s not written by an LLM, which I find somewhat refreshing :)
Sounds like an interesting direction to me, rants about Hoare et al. notwithstanding, and cool to see Isabelle-proofs as part of the release.
I think
⌊post_p⌋ = post_⌊p⌋
Which I think is this?
post_p / (Pre_p ∩ C)
but yeah, rounding is defined in the article only for programs, not for postconditions.
I’m skeptical about what this article contributes to the field (has this really not been done before?), but I could believe that building a theory of computation directly on set theory would be convenient for reusing set theory ideas and tools in computation theory.
I think it’s actually complex mathematics
This is simple vs. easy. It definitely is very simple mathematics, pretty basic set theory (not Venn diagram basic, as it needs functions&relations, but nothing even remotely crazy). It probably isn’t easy for most people, as I think this “foundations of mathematics” stuff is not frequently taught, and it does require somewhat more abstract thinking.
Perhaps even the question itself is a type error. Sure, programming is mostly done via Turing-complete languages, and a Turing-completeness is surprisingly easy/trivial to reach. (Doesn’t make “the sum of its parts” any easier though, two trivial function’s composition may not end up as a trivial function.)
As for why I consider it a type error: programming is the whole act and art of building and maintaining computable functions with certain properties, if we want to be very abstract.
Naming variables, encoding business logic/constraints in a safe way, focusing on efficiency are all parts of programming itself. The computing model is just one (small) part of it all.
Programming is the art of understanding a process in enough detail that a computer can be used to automate part of it.
Related:
https://lockywolf.wordpress.com/2019/02/16/a-mathematical-theory-of-systems-engineering-the-elements-by-a-wayne-wymore/
More like complicated mathematics.
No mention at all of TLA+ in the paper? TLA+ has no known axioms it relies on to my knowledge. It’s also just “simple math”, i.e. set theory and predicate logic. I didn’t see anything that was all that different from TLA+ here, except TLA+ talks way more about actual program execution, which I didn’t see that much of here.
I mean I like the idea, for the same reason that I like TLA+: it’s actually digestible. Set theory really is simple and understandable, vs. something like dependent type theory.
I just didn’t understand some of the criticisms, for example how is this definition of refinement different than any others? It seems like the same thing.
I think TLA⁺ does have axioms, since it has to define what the temporal logic of actions is. So in A Science of Concurrent Programs Lamport goes through simpler constructions like the “Logic of Actions” which introduces sequences of states indexed by a time parameter, then on to “Raw Temporal Logic of Actions” which gets rid of the time parameter and defines the □ operator, finally ending up at the “Temporal Logic of Actions” which requires formulas to be stuttering-insensitive so introduces □[A]ᵥ and ◇⟨A⟩ᵥ. It all ultimately is built on top of the Kahn model mentioned in this paper where variables are mapped to specific values in a given state.
Lamport also cautions that TLA is weirder than ordinary predicate logic on page 69 of A Science of Concurrent Programs:
You’re right TLA⁺ does have a simple definition of refinement, where a system described by TLA formula P refines a system described by TLA formula Q if P ⇒ Q. However, this isn’t really unique; actually Exercise 9 of Chapter 1.1 (Volume 1) of The Art of Computer Programming has you invent a set-theoretic definition of refinement whole-cloth (it’s a fun exercise, take a look at it!).
yea, I was mistaken, TLA does have axioms (figure 5 in section 5.6 in Temporal Logic of Actions).
I’ll check out that exercise at some point. I’m in the “refinement is one of the most important ideas in CS” camp, so any deeper insight there is always welcome.
I am aware of some limitations of refinement, for example a program which does nothing (has no observable behaviors) refines every program vacuously. But this is just a consequence of refinement being defined in terms of subset / implication: the empty set is a subset of everything, false implies true, etc.
But I didn’t see how these refinement definitions had any benefit so far.
The vacuous refinement case is annoying because it’s definitely possible to accidentally write an inconsistent fairness constraint ensuring your program generates zero behaviors, thus vacuously satisfying any refinement relation you’re trying to check. I proposed adding a warning if this happens: https://github.com/tlaplus/tlaplus/issues/161
The approaches «relying» on large sets of axioms and/or reasoning rules often come with models and pretty easy soundness proofs. Consistency/nontriviality is not as much of an issue as claimed.
The reason to go with weirdly carved axioms despite having a model is to have proof tools (sometimes in the sense of lemmas, sometimes in the sense of software) suitable for everything that is expressible at all. Arbitrary set theory claims are sometimes needed but don’t make proof tools easy…
Hm, so is there an example of how a correctness argument for a particular program would look under this formalism?