Dafny seems to have loops too, and the way it solves the problem you mentioned is forcing the user to write these invariants.
I assume if you were to develop such a system for C, C++, or Rust you'd similarly expect the user to do this.
I assume if you were to develop such a system for C, C++, or Rust you'd similarly expect the user to do this.
(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.
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.