Right. The problem is that those languages are relatively permissive in their type systems. Obviously Rust can capture more in its type system than C can. You would probably want a type like “decreasing unsigned integer” for Rust and some way to enforce monotonic decreasing, which Rust doesn’t give you.

(Any experts on formal verification please correct any inaccuracies in what I say here.)

The upshot of it is that C, C++, and Rust permit too much behavior that isn’t capturable in the type system. Thus, the properties that you’re interested in are semantic (as opposed to syntactic; type systems turn semantic properties into syntactic ones) so Rice’s theorem applies and there’s no computable way to do the analysis right.

You are answering a question you want to answer, not the one I asked! :)

Yes, dependent types can encode nice constraints, but so can asserts and assumes.

I am not seeing the fundamental difference in yeeting these constraints to a solver. Dafny seems to do the same thing with Z3.