> is static analysis really more powerful than the Rust type system + borrow checker?

Yes, and by far. A theorem prover, as the name suggests, can be used to prove algorithmic correctness of your code.

There’s no model more powerful than static analysis if, by static analysis, they mean abstract interpretation: the Galois connection guarantees this.

> abstract interpretation

That's not what static analysis (which includes things like type-checking) means and that's not something you can do with general-purpose code, for reasons related to Rice's theorem.

Type-checking is one of the classical examples of abstract interpretation — it's mentioned in the original Cousot & Cousot paper (1977). Maybe you're thinking of something else?

Static analysis is more than just abstract interpretation, and the OP doesn't discuss abstract interpretation at all, but talks about a design by contract approach inspired by Ada/SPARK.

Maybe not directly mentioned in the article, but I think abstract interpretation is happening...

It's talking about DrNim, and docs page for that https://nim-lang.org/docs/drnim.html says:

"DrNim combines the Nim frontend with the Z3 proof engine in order to allow verify / validate software written in Nim"

So I think the design-by-contract annotations are being checked via abstract interpretation (that's what gets fed into Z3 I think?)

Z3 is a contraint solver (SMT, SAT) which makes total sense to use in a design by contract system, but AFAIK there is zero link to abstract interpretation (which from what I understood about it, is way harder to use).

How else are you going to check the contracts at compile time?

I honestly don't know if that's how DrNim works or if there are other ways to achieve that.

But a similar tool for Python does it exactly this way: https://github.com/pschanely/CrossHair "CrossHair works by repeatedly calling your functions with symbolic inputs. It uses an SMT solver (a kind of theorem prover) to explore viable execution paths and find counterexamples for you."

...so that's where I got the idea that DrNim is probably doing the same