[win311fwg]

Formal verification is also extremely common in the software design world, to be fair. Most programming languages in use have at least a primitive type system and even those that historically didn't are gaining them (e.g. Typescript, Python gradual typing, etc.)

The question is, as always, to what degree do the returns start to diminish. The Rust crowd laughs at Go's level of formal verification and says that their level of formal verification is the right level, but then the Lean crowd laughs at Rust's level of verification and says that their level of formal verification is the right level. The universe laughs at all of them. For crowds so concerned about mathematical proofs, it is funny that they end up right back at gut feeling.

[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?