[MichaelSalib]

Formal verification allows you to prove that an implementation faithfully implements its specification. What does the formal specification for a web browser look like? I'm guessing that we're talking about thousands of pages of extremely dense math and code. How do you know that that specification is correct, or reasonable or what the user wants?

Now, maybe we don't want to do formal verification for correctness because it is too hard. So we settle for formally verifying that a program has some property of interest, like memory safety. But if you want memory safety, it is a lot cheaper to just use a language that gives you memory safety for free (haskell/scala/go/python) rather than trying to formally verify that your C++ program is memory safe.