2
$\begingroup$

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?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.