alt Hacker NewsSpecifying that a value must be an integer between 1 and 10 is most certainly further along the continuum than only specifying that a value must be an integer, but both define a theorem about the program that can be validated. How is the latter not formal verification? It's the same thing, only differing by degree.
As I said, it's a continuum. I'm drawing the line somewhere further along it than Rust's type system.