In our community we often say that we have formally verified something, but e.g. wikipedia has a wider meaning for that.

https://en.wikipedia.org/wiki/Formal_verification

Do people have a preference for a more precise term?

Well, this Wikipedia page says "The verification of these systems is done by providing a formal proof".

And the Wikipedia page of "formal proof" says "It differs from a natural language argument in that it is rigorous, unambiguous and mechanically checkable."

I think the community has shown preference in the past for "machine-checked proofs (of correctness)", and I think *machine checkable* or *machine checked* is definitely to be preferred over *mechanized*, which outsiders typically don't understand what it means.

basically, the definition of "formal proof" as proofs that are *mechanically checkable*, is not even agreed on in theoretical computer science. I regularly meet theory A researchers who consistently claim they provide "formal proofs". One way to guard oneself is to qualify: "a formal proof **in Coq**"

I've recently reviewed a paper in SE which claimed providing a "formal proof" in its abstract. I reminded the authors that, at least in the PLSE communities, "formal proof" usually means something more specific.

Another alternative is "program proof" as argued in this post by Nik Swamy: https://blog.sigplan.org/2019/09/12/program-verification-has-it-lost-its-punch/

the problem is that a lot of work in the Coq community is not really about verifying programs (at least not what the CS community usually means by "program")

the Coq Feit-Thompson theorem paper was called: "A Machine-Checked Proof of the Odd Order Theorem". I think this is a good example to follow. In contrast, proofs in many program verification systems (e.g., Dafny) are not machine-checked.

"not machine-checked" seems likely to cause confusion. For this distinction, https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf talks about "foundational machine-checked proofs" (and defines it right away)

And given the context, I assume that's to distinguish those proofs from those by program verifiers using separation logic (but not foundationally)

the definition in that paper is for PL only, so I don't see how it generalizes outside PL. I also think it's usually very clear when a tool has no proofs to check by machine. For example, Dafny basically just outputs a diagnostic message when it succeeds "proving" something.

The more general part is > assuming only the low-level axioms of mathematical logic

And when comparing to Dafny you can use the full definition.

Conversely, while I see what you mean, here's an example of confusion at SOSP (a top conference) http://sigops.org/s/conferences/sosp/2015/current/2015-Monterey/printable/250-hawblitzel.pdf

We provide the first machine-verified liveness proofs of non-trivial distributed system

As in our previous work [21], we use Dafny [39], a high- level language that automates verification via the Z3 [11] SMT solver

Or https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml231.pdf

I guess that for them, the Dafny output is the result of "machine-checking" the "proofs"

In any case, I don't suppose that a standard term exists that doesn't need explanations; there seems to be inflation. It's better to document and compare assumptions.

One of the things in the story of the Odd Order thm is that that proof was studied, and checked, by mathematicians for quite some time before it became accepted. I think machine-checked v.s. human-checked is the first point, and it also applies to the Flyspec project (IIRC there human reviewers just gave up).

essentially the same authors as the SOSP paper are now making new quite strong claims about using Dafny for verifying concurrent programs (which I think they could have toned down given Dafny's quite humble foundational status):

a new coding language and tool for high-performance concurrent programs that ensures that programs are provably-correct – that is, that the code is mathematically proven to compute correctly.

To reiterate from above, the implication of "mathematically proven" in that context should (in my opinion) be that they are able to produce an artifact someone can straightforwardly and independently check by computer (and a theory of Dafny's foundations would be nice as well...)

as I think we've discussed before, I think this page in the wiki needs an update: https://github.com/coq/coq/wiki/Presentation#what-do-i-have-to-trust-when-i-see-a-proof-checked-by-coq -- but maybe every CPP paper should come with a disclaimer similar to that?

Their "limitations" does discuss this assumption and links to how to compile it away; I have no comment on whether that's actually sound.

I feel compelled to mention that, in part due to Andrej Bauer, every time I see the phrase "provably correct" in print I get a little upset

http://math.andrej.com/2015/08/05/provably-considered-harmful/

it's incredible how it is standard phrasing in this kind of work

About texts that make us unhappy: Is anyone unhappy with this text (from the wiki page linked above)

```
What is Coq?
The Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows:
the definition of mathematical objects and programming objects,
to state mathematical theorems and software specifications,
to interactively develop formal proofs of these theorems,
to check these proofs by a small certification “kernel”.
Coq is based on a logical framework called “Calculus of Inductive Constructions” extended by a modular development system for theories.
```

What is a "programming object" and what is a "logical framework extended by a modular..."?

If tell me that out of the Coq wiki context, then I think you talk about Twelf.

Also I don't care about LOC more than I care about H-index, but "small" is a bit of a lie.

Yes, the page is careful lacking citations. A bit more discussion here:

https://coq.discourse.group/t/why-is-coq-consistent-what-is-the-intended-semantics/347/22

"Measuring programming progress by lines of code is like measuring aircraft building progress by weight.” (Bill Gates)

maybe it's all a funding trick to write "provably correct" in every paper, so one can say in grant applications: "we will go from 'provably' to 'proven' correct". Then just keep writing "provably" and repeat.

Last updated: Oct 12 2024 at 13:01 UTC