Max Kirchmeier (Sep 29 2020 at 13:20): Max Kirchmeier (Sep 29 2020 at 13:20):Hi there,
I'm fairly new to Coq and currently trying to understand part of CompCert's code, specifically Mem.free.
It seems like it's using a lemma as a predicate inside the if... how does that work?
Karl Palmskog (Sep 29 2020 at 13:23):@Max Kirchmeier the Lemma keyword doesn't indicate anything fundamental in Coq. You can in principle take any Coq code and replace Lemma with Definition. In this case, it happens that the "lemma" actually is a decision procedure
Max Kirchmeier (Sep 29 2020 at 13:26):@Karl Palmskog Ah, thanks. That means I'd have to actually understand the {...} + {~...} syntax then, any pointers what that means? :D
Karl Palmskog (Sep 29 2020 at 13:27):see sumbool here: https://coq.inria.fr/distrib/V8.12.0/stdlib/Coq.Init.Specif.html#sumbool
Karl Palmskog (Sep 29 2020 at 13:32):@Max Kirchmeier unfortunately, learning Coq by looking at CompCert is not going to be straightforward at all. Consider reading one of the books on Coq: https://github.com/coq-community/awesome-coq#books
In particular, Software Foundations Book 1 is targeted at early learners. Sumbools are discussed here.
Max Kirchmeier (Sep 29 2020 at 13:45):Ah! Thanks a lot, this explains quite a bit :)
I'm mainly interested in understanding CompCert's code for the purpose of porting the basics to Isabelle (see here), so it made sense to start with looking at the project instead of learning Coq first. But it seems there are some fundamental differences in the concepts between Coq and Isabelle, so I might have to rethink that approach.
Karl Palmskog (Sep 29 2020 at 13:48):you could probably get away with only learning fundamentals, such as Coq sorts, universes, etc., instead of the whole Stdlib and so on. But constructive type theory is indeed very different from HOL. One thing that might help is to look at Isabelle/CTT
Karl Palmskog (Sep 29 2020 at 13:55):also, as you might already know, Thomas Sewell (then at NICTA) looked at porting CompCert to Isabelle back in 2011-2012. In the end, he decided to go with binary translation validation instead, I believe mainly due to foundational incompatibility.
Karl Palmskog (Sep 29 2020 at 14:00):see also this for a super-high-level summary of foundational differences between Coq and HOL: https://coq.discourse.group/t/why-doesnt-coq-have-a-theorem-type-like-hol-light/532/4
Max Kirchmeier (Sep 29 2020 at 14:37):That's really interesting, I actually hadn't heard of Thomas Sewell's attempt at this before! Though thankfully it sounds like the differences between Coq and HOL might have only been the lesser part of the problem. Nevertheless, I hope I won't run into any serious incompatibilities...
Your post about the foundational differences is also quite illuminating; I'd wondered why types were built through "functions" in Coq.
So it seems Coq is, in principle, the more powerful tool. I'm wondering however, are there often instances where these capabilities are actually necessary? The feeling I have so far is that, although the more complex concepts Coq can represent are hard (or impossible) to represent in HOL, for the "average proof" HOL might be easier to work with. What are your thoughts/experiences in that regard?
Karl Palmskog (Sep 29 2020 at 14:44):The usefulness of dependent types (vs. simple types as in HOL) is an endlessly debated topic in the community. One recent discussion thread is here: https://coq.discourse.group/t/why-dependent-type-theory/657
Karl Palmskog (Sep 29 2020 at 14:45):personally, I use both Coq and HOL4. In both cases, it was motivated by access to certain libraries, not any dedication to a certain foundation.
Bas Spitters (Sep 29 2020 at 14:49):https://bedrocksystems.com/ chose Coq over Isabelle for verifying a hypervisor. I can speculate why, but @Gregory Malecha or @Abhishek Anand will have more details.
Karl Palmskog (Sep 29 2020 at 14:53):I'm sure there will be someone soon who refuses anything but cubical type theory for a verification project... In the end, one would have to establish by empirical studies what foundations are suitable for which tasks, but holding stuff like developer experience constant is likely to be near-impossible
Paolo Giarrusso (Sep 29 2020 at 16:08):We're already a bit OT, but we at Bedrock currently use Iris (I cannot comment on the past history), and apparently it's unclear how to port it to HOL:
https://mattermost.mpi-sws.org/iris/channels/town-square/sgrt5ccp9py7bpwj9docawi3pc
Paolo Giarrusso (Sep 29 2020 at 16:10):and an (out-of-context?) quote of https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324036/ writes:
For example, it is challenging to define subalgebras and to impose additional algebraic structure on a subset of an algebra.
Paolo Giarrusso (Sep 29 2020 at 16:12):I'm sure alternatives exist, and that intro mentions some, but I wouldn't have expected challenges for something as mundane as substructures
Christian Doczkal (Sep 30 2020 at 09:40):Max Kirchmeier said:
So it seems Coq is, in principle, the more powerful tool. I'm wondering however, are there often instances where these capabilities are actually necessary? The feeling I have so far is that, although the more complex concepts Coq can represent are hard (or impossible) to represent in HOL, for the "average proof" HOL might be easier to work with. What are your thoughts/experiences in that regard?
My favorite example for this is deterministic finite automata. Mathematically, one has a tuple (Q,s,d,F) where Q is some set whose internal structure is irrelevant most of the time, s is an element of Q, d is a function from Sigma x Q to Q, and F is a subset of Q. The "natural" formulation in Isabelle/HOL (Paulson, https://www.isa-afp.org/entries/Finite_Automata_HF.html) involves hereditariliy finite sets, pre-automata, and heaps of side conditions. In Coq this can be simply represented using a (dependent) record type without any side conditions (myself :smile: , https://github.com/coq-community/reglang/blob/d3140eb9ae4027d4e0619142746368175c81259c/theories/dfa.v#L16).
Max Kirchmeier (Sep 30 2020 at 12:41):Thank you all for the answers! That DFA example is great, that's exactly the kind of easily-accessible proof I was wondering about :)
Last updated: Oct 13 2024 at 01:02 UTC