[mafribe]

Since there is often a misconception that formally verified software must be absolutely free from problems, from the conclusion of the paper: "Extensive testing on formally verified software is necessary for at least two reasons. First, the formal specification may not guarantee all the properties expected by users, but only critical ones (e.g. no miscompilation for CompCert). Second, critical bugs may still remain, because the formal specification might not exactly fit reality. However, in this case, critical bugs are in the—much smaller and simpler—[trusted computing base]"

[DonaldPShimoda]

An excellent clarification to make.

"Formally verified software" means that some portion of the software's expected behavior has been rendered as a proposition, and that proposition has been proven correct using some kind of proof assistant or theorem-proving software that we assume correctly validates the proof of the proposition. Bugs can exist in three places, then:

1. Within the theorem-proving software. 2. Within the proposition itself. 3. Within the portions of the code that are not formally verified.

We generally have good reason to suspect bugs in (1) are almost nonexistent. Bugs in (2) and (3) are relatively common, but (3) is no different from the bugs present in software with no formal verification.

A lot of modern theorem-proving research lies in helping people to address bugs in (2) by making propositions easier to write and verify, and in (3) through the same mechanism (because then we can formally verify a greater portion of the software).

[astrange]

> "Formally verified software" means that some portion of the software's expected behavior has been rendered as a proposition, and that proposition has been proven correct using some kind of proof assistant or theorem-proving software that we assume correctly validates the proof of the proposition.

All programs that don't contain undefined behavior satisfy this (in an annoying tautological way) because all programs are proofs of themselves. So the thing you're getting paid for, if you are, is to ask the right questions of your theorem prover (which may be a Python interpreter).

[wtroughton]

A compiler is a theorem prover, sure, but compilers vary in terms of expressiveness of the propositions it is capable of proving (a Python interpreter would be a very weak theorem prover ;) )

Consider: is there an equivalent concept of Turing Completeness for compilers with respect to computational propositions?

[DonaldPShimoda]

I know what you're saying, but there's a difference between "the expected behavior has been rendered as a proposition" (what I said) and "the expected behavior corresponds with a proposition" (what you're saying).

To "render something as a proposition" means for it to be literally written down in the terms of formal logic. Writing a program in Python doesn't generally constitute this form of expression, but writing a proof of a Python program would.