[IshKebab]

It's a continuum... but I would say even Rust's type system is not in the realms of "formal verification". I think you need at least some kind of refinement types so you can say "an integer between 1 and 10" before you can stake even a vague claim to "formal verification".

So I don't think you can say it's common in the software world.

[win311fwg]

Specifying 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.

[IshKebab]

As I said, it's a continuum. I'm drawing the line somewhere further along it than Rust's type system.

[win311fwg]

Understood. In dynamic verification, does that same line hold? Or would you say it is it unique to formal verification? If so, why?

[IshKebab]

First I've heard of "dynamic verification" tbh. Is that just everything that isn't static analysis? Not sure I understand the question!

[win311fwg]

You may also know of it as standard verification or empirical verification. Regardless of the name, I am sure you can understand the concept as it is exactly of the same intent as formal verification (e.g. you might seek to ensure that a value is an integer between 1 and 10), but absent the formal methods. Of course, just as you can seek to verify that a value is between 1 and 10 you can also simply verify that a value is an integer.

Therefore the possibility of the same dividing line exists in that space as well, but I was wondering if you recognize the same dividing line there, or if it is unique to where formal methods are used?