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?

@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

@Karl Palmskog Ah, thanks. That means I'd have to actually understand the `{...} + {~...}`

syntax then, any pointers what that means? :D

see `sumbool`

here: https://coq.inria.fr/distrib/V8.12.0/stdlib/Coq.Init.Specif.html#sumbool

@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.

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.

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

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.

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

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?

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

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.

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.

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

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

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.

I'm sure alternatives exist, and that intro mentions some, but I wouldn't have expected challenges for something as mundane as substructures

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).

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: Feb 01 2023 at 11:04 UTC