Bas Spitters (Jul 31 2020 at 06:37): Bas Spitters (Jul 31 2020 at 06:37):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?
Théo Zimmermann (Jul 31 2020 at 07:07):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."
Karl Palmskog (Jul 31 2020 at 10:55):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.
Karl Palmskog (Jul 31 2020 at 10:59):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"
Théo Zimmermann (Jul 31 2020 at 11:22):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.
Kartik Singhal (Jul 31 2020 at 21:12):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/
Karl Palmskog (Jul 31 2020 at 21:20):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")
Karl Palmskog (Aug 01 2020 at 12:28):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.
Paolo Giarrusso (Aug 01 2020 at 17:36):"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)
Paolo Giarrusso (Aug 01 2020 at 17:37):And given the context, I assume that's to distinguish those proofs from those by program verifiers using separation logic (but not foundationally)
Karl Palmskog (Aug 01 2020 at 17:49):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.
Paolo Giarrusso (Aug 01 2020 at 18:08):The more general part is > assuming only the low-level axioms of mathematical logic
Paolo Giarrusso (Aug 01 2020 at 18:08):And when comparing to Dafny you can use the full definition.
Paolo Giarrusso (Aug 01 2020 at 18:11):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
Paolo Giarrusso (Aug 01 2020 at 18:11):We provide the first machine-verified liveness proofs of non-trivial distributed system
Paolo Giarrusso (Aug 01 2020 at 18:12):As in our previous work [21], we use Dafny [39], a high- level language that automates verification via the Z3 [11] SMT solver
Paolo Giarrusso (Aug 01 2020 at 18:18):Or https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml231.pdf
Paolo Giarrusso (Aug 01 2020 at 18:19):I guess that for them, the Dafny output is the result of "machine-checking" the "proofs"
Paolo Giarrusso (Aug 01 2020 at 18:20):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.
Enrico Tassi (Aug 01 2020 at 18:28):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).
Karl Palmskog (Aug 01 2020 at 18:45):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...)
Karl Palmskog (Aug 01 2020 at 18:53):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?
Paolo Giarrusso (Aug 01 2020 at 19:22):Their "limitations" does discuss this assumption and links to how to compile it away; I have no comment on whether that's actually sound.
Pierre-Marie Pédrot (Aug 02 2020 at 07:59):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/
Pierre-Marie Pédrot (Aug 02 2020 at 07:59):it's incredible how it is standard phrasing in this kind of work
Enrico Tassi (Aug 02 2020 at 09:39):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.
Enrico Tassi (Aug 02 2020 at 09:41):Also I don't care about LOC more than I care about H-index, but "small" is a bit of a lie.
Bas Spitters (Aug 02 2020 at 11:52):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
Bas Spitters (Aug 02 2020 at 11:53):"Measuring programming progress by lines of code is like measuring aircraft building progress by weight.” (Bill Gates)
Karl Palmskog (Aug 02 2020 at 14:07):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: Apr 18 2024 at 11:02 UTC