Also:

- Have a clear notion of what part of the specs represents the system under your control (the "machine"), and what part represents the broader world it interacts with. The world can do more than the machine, and the properties on the world are much more serious.

- Make lots of helpers. You need them more than you think.

- Add way more comments than you normally would. Specs are for analyzing very high-level ideas, and you should be explaining your high-level ideas.

- Make the spec assumptions clear. What has to be true about the operating environment for the spec to be sensible in the first place?

- Use lots of model values, use lots of constants, use lots of ASSUME statements. Constrain your fairness clauses as narrowly as possible.

- Understand the difference between the semantics of TLA+ as an abstract notation and the semantics of TLA+ as something concretely model-checked. For example, TLA+ is untyped, but the model checker is typed. Also, a lot of TLA+ features are not available in different model checkers. OTOH, you can break TLA+ semantics with use of TLCSet and TLCGet.

The last tip applies to whatever modeling language you use: most have the same distinction.

I've had to help a client with something not exactly like, but with similar properties as, Google Docs. One of the big properties they had to engineer in was "the doc should eventually look the same for all open browser tabs on the same computer".

The other big question: what happens if user A makes change X and user B makes change Y? There's a lot of outcomes the product can pick between, but whatever they pick it should be consistent. That consistency in conflict resolution is a good property to model.

I think the "high school math" slogan is untrue and ultimately scares people away from TLA+, by making it sound like it's their fault for not understanding a tough tool. I don't think you could show an AP calculus student the equation `<>[](ENABLED <<A>>_v) => []<><<A>>_v` and have them immediately go "ah yes, I understand how that's only weak fairness"

Oh, hey -- you're that guy. I learned a lot of what I know about TLA from your writings ^_^

Consider my behavior changed. I thought the "high school math" was an encouraging way to sell it (i.e. "if you can get past the syntax and new way of thinking, the 'math' is ultimately straight forward"), but I can see your point, and how the perception would be poor when they hit that initial wall.

I really do wish that PRISM can one day add some quality of life features like "strings" and "functions"

(Then again, AIUI it's basically a thin wrapper over stochastic matrices, so maybe that's asking too much...)

> No problem with floats or strings as far as specification goes. The particular verification tools you choose to run on your TLA+ spec may or may not have limitations in these areas, though.

I think it's disingenuous to say that TLA+ verifiers "may or may not have limitations" wrt floats when none of the available tools support floats. People should know going in that they won't be able to verify specs with floats!

I'm not sure how a "spec with floats" differs from a spec with networks, RAM, 64-bit integers, multi-level cache, or any computing concept, none of which exists as a primitive in mathematics. A floating point number is a pair of integers, or sometimes we think about it as a real number plus some error, and TLAPS can check theorems about specifications that describe floating-point operations.

Of course, things can become more involved if you want to account for overflow, but overflow can get complicated even with integers.

Those things, unlike floats, have approximable-enough facsimiles that you can verify instead. No tools support even fixed point decimals.

This has burned me before when I e.g needed to take the mean of a sequence.

You say no tools but you can "verify floats" with TLAPS. I don't think that RAM or 64-bit integers have facsimiles in TLA+. They can be described mathematically in TLA+ to whatever level of detail you're interested in (e.g. you have to be pretty detailed when describing RAM when specifying a GC, and even more when specifying a CPU's memory-access subsystem), but so can floating point numbers. The least detailed description - say, RAM is just data - is not all that different from representing floats as reals (but that also requires TLAPS for verification).

The complications in describing machine-representable numbers also apply to integers, but these complications can be important, and the level of detail matters just as it matters when representing RAM or any other computing concept. Unlike, say, strings, there is no single "natural" mathematical representation of floating point numbers, just as there isn't one for software integers (integers work differently in C, Java, JS, and Zig; in some situations you may wish to ignore these differences, in others - not). You may want to think about floating point numbers as a real + error, or you may want to think about them as a mantissa-exponent pair, perhaps with overflow or perhaps without. The "right" representation of a floating point number highly depends on the properties you wish to examine, just like any other computing construct. These complications are essential, and they exist, pretty much in the same form, in other languages for formal mathematics.

P.S. for the case of computing a mean, I would use Real rather than try to model floating point if the idiosyncracies of a particular FP implementation were important. That means you can't use TLC. In some situations it could suffice to represent the mean as any number (even an integer) that is ≥ min and ≤ max, but TLC isn't very effective even for algorithms involving non-tiny sets of integers when there's "interesting" arithmetic involved.

I don't know the state of contemporary model checkers that work with theories of reals and/or FP, and I'm sure you're much more familar with that than me, but I believe that when it comes to numeric computation, deductive proofs or "sampling tests" (such as property-based testing) are still more common than model-checking. It could be interesting to add a random sampling mode to TLC that could simulate many operations on reals using BigDecimal internally.

Thanks for sharing the general term! I didn't know about it.

Now you just gotta go to the first submission and post a link here. Complete the circle!

The principle of causality actually prevents time from forming closed loops in which time would run in a circle.

Since writing this I've been informed of some gaps (mostly through email and a lobsters [1] thread). Some of the main ones:

- McCarthy's "Direct Union" is probably conflating "disjoint union" and "direct sum".

- ML probably got the sum/product names from Dana Scott's work. It's unclear if Scott knew of McCarthy's paper or was inspired by it.

- I called ALGOL-68 a "curious dead end" but that's not true: Dennis Ritchie said that he was inspired by 68 when developing C. Also, 68 had exhaustive pattern matching earlier than ML.

- Hoare cites McCarthy in an earlier version of his record paper [2].

Also I kinda mixed up the words for "tagged unions" and "labeled unions". Hope that didn't confuse anybody!

[1] https://lobste.rs/s/ppm44i/very_early_history_algebraic_data...

[2] https://dl.acm.org/doi/10.5555/1061032.1061041

I love how you create dataclasses to abstract over constraints!

Even worse than that, SMT can encode things like Goldbach's conjecture:

    from z3 import \*

    a, b, c = Ints('a b c')
    x, y = Ints('x y')
    s = Solver()

    s.add(a > 5)
    s.add(a % 2 == 0)
    theorem = Exists([b, c],
                     And(
                         a == b + c,
                         And(
                             Not(Exists([x, y], And(x > 1, y > 1, x \* y == b))),
                             Not(Exists([x, y], And(x > 1, y > 1, x \* y == c))),
                             )
                         )
                     )

    if s.check(Not(theorem)) == sat:
        print(f"Counterexample: {s.model()}")
    else:
        print("Theorem true")