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 an hour ago | parent [-]

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 32 minutes ago \| parent [-]
		Specifying that a value must be an integer between 1 and 10 is most certainly further down 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.