I agree with everything you've said, and about refinements in particular. TLA+ newcomers often think of refinement as an advanced tool, but it's one of the most pragmatic and effective ways to specify.

But I'd like to add some nuance to this:

> And pure maths that can be exhaustively checked by the computer? It’s not as perfect as a proof but it’s great for a lot of practical applications.

1. A run of a model checker is exactly as perfect as a proof for the checked instance (which, indeed, is a weaker theorem than one that extends to an unbounded set of instances). In fact, it is a proof of the theorem when applied to the instance.

2. A proof is also not perfect for real software. A proof can perfectly convince us of a correctness of an algorithm, which is a mathematical construct, but a software system is not an algorithm; it's ultimately a physical system of silicone and metal elements that carry charge, and a physical system, unlike an algorithm, cannot be proven correct for the simple reason it's not a mathematical object. Virtually all correctness proofs assume that the hardware behaves correctly, but it only behaves correctly with high probability. My point is only that, unlike for algorithms or abstract theorems, there can be no perfect correctness in physical systems. Increasing the confidence in the algorithm beyond the confidence in the hardware (or human operators) may not actually increase the confidence in the system.

Absolutely, I was waving my hands a lot there. Thanks for adding that.

And I’d also add the small model theory from Software Abstractions: if there is an error in your spec in a large instance then it is likely also going to appear in a small one. Most of errors can be caught by small instances of a model.

I only mention it because the common retort when people find out that the model checker only exhaustively checks a limited instance is, software is complex and you can’t model everything.

It’s true. But we don’t need models that account for the gravitational waves in our local region of space to get value from checking them. And neither do most programmers when they use unit tests or type checkers.

And proofs… I think I might disagree but I don’t have the professional experience to debate it fully. I do know from a colleague who does proof engineering on a real system written in C++ that it’s possible however… and likely more difficult than model checking.