I have a vague understanding what formal verification is about, a vague understanding of what the cutting edge is of type theory for programming languages, and a better understanding of formal proofs.
So far as I understand, the purpose of formal verification is to (1) specify a set of “desired properties” in the form of logical propositions about a system/program, and (2) use some kind of logic to check those propositions.
Similarly, using type theory (especially with the curry-howard isomorphism) we can also to (1) specify a set of “desired properties” of a program, and (2) by type-checking ensure that those properties hold.
Formal proof seems to underly both.
What is the relation between these three things?
What kind of properties of programs/systems can we check with modern state-of-the-art type systems?
is type theory an example of “formal verification” or does the latter term not include it?
What are the advantages and disadvantages of (classical?) formal verification versus type theory-based checking of program properties?
