hwayne

The key bit is that specifications don't need to be "obviously computable", so they can be a lot simpler than the code that implements them. Consider the property "if some function has a reference to a value, that value will not change unless that function explicitly changes it". It's simple enough to express, but to implement it Rust needs the borrow checker, which is a pretty heavy piece of engineering. And proving the implementation actually guarantees that property isn't easy, either!

...Whoops. Yup, SMT solvers can famously return `unknown` on top of `sat` and `unsat`. Just added a post addendum about the mistake.

I'll warn you that Picat is very much a "research language" and a lot of the affordances you'd expect with a polished PL just aren't there yet. There's also this really great "field notes" repo from another person who learned it: https://github.com/dsagman/picat

Check out datalog! https://learn-some.com/ The tutorial there uses Clojure syntax but Datalog normally uses a Prolog syntax.

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"

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.

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!

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!

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")

It really depends on the kind of solving you want to do. Mathematical optimization, as in finding the cheapest/smallest/whatever solution that fits a problem? OR-Tools. Satisfaction problems, like finding counterexamples in rulesets or reverse engineering code? Z3.

Now I'm mad I didn't remember the word "antics". It's so much more evocative than "crimes"!

Entertaining collection of Folklore classifications. Some examples:

- T550.6. T550.6. Only half a son is born by queen who ate merely half of mango.

- A1066. A1066. Sun will lock moon in deep ditch in earth's bottom and will eat up stars at end of world.

- K87.1. K87.1. Laughing contest: dead horse winner.

Main way we're validating that now is by using TLA+ models to generate test suites. Mongo came out with a new paper on this recently: https://will62794.github.io/assets/papers/mdb-txns-modular-v...

If you put the spec online I'd be happy to give it a quick optimization skim!

Apparently they're getting very good: https://emschwartz.me/new-life-hack-using-llms-to-generate-c...

I try not to use them too much because I want to build the skill of using SMTs directly for now.

I remember you showing me this! Wow that was a long time ago.

My favorite is the third place, "Cornelia". Mostly because I feel like it's something that could have been made in the Renaissance and would have been considered among the Greatest Art of All Time if it was.

I think of the two P-lang probably has a brighter future. I don't know how many people are working on Spin besides Holzmann, while P has a lot of institutional support and development budget at AWS.

Right now the best practice is generating test suites from the TLA+ spec, though right now it's bespoke for each company that does it and there's no production-ready universal tools do that. LLMs help.

With one client I have, we know the TLA+ model is accurate because we're extracting tests directly from the spec. It's kind of a riff on what MongoDB does in this paper: https://arxiv.org/abs/2006.00915

This is a quick demo of TLA+ I like: https://gist.github.com/hwayne/39782de71f14dc9addb75f3bec515...

It models N threads non-atomically incrementing a shared counter, with the property "the counter eventually equals the number of threads in the model". When checked in TLA+, it finds a race condition where one threads overwrites another value. I've written implementations of the buggy design and on my computer, they race on less than 0.1% of executions, so testing for it directly would be very hard.

Most TLA+ specs are for significantly more complex systems than this, but this is a good demo because the error is relatively simple.

`S = {str -> bool}` is actually uncountable. `S` is isomorphic to the power set (set of all subsets) of `str`, and `2^str` is at least as big as the set of real numbers, as any real number (like π) can be mapped to the set of string prefixes (like `{"3", "3.1", "3.14", ...}`). Since the reals are uncountable, so is `2^str` and `S`.

That's not necessarily true. Consider the program `x := 4; loop {if !sum_of_two_primes(x) {return true}; x += 2}`. If we run this on a general purpose CPU, this will halt if and only if Goldbach's conjecture has a counterexample. Otherwise it will run forever. So even if a working halt detector takes 14 million billion years, it will definitely tell us if the conjecture is true or not. Whereas if the general purpose CPU is still running after that time, we still have no way of knowing whether it's because it's going to run forever or if it simply hasn't reached the first (ludicrously large) counterexample.

A couple of useful general approaches:

- "Metamorphic testing" is where analyze how code changes with changing inputs. For example, adding more filters to a query should return a strict subset of the results, or if a computer vision system recognizes a person, it should recognize the same person if you tilt the image.

- Creating a simplified model of the code, and then comparing the code implementation to the model, a la https://matklad.github.io/2024/07/05/properly-testing-concur... or https://johanneslink.net/model-based-testing

There's also this paper, which I haven't read yet but seems intriguing: https://andrewhead.info/assets/pdf/pbt-in-practice.pdf