Stream: Coq devs & plugin devs

Topic: Verified Kernel


view this post on Zulip Jason Gross (Sep 07 2020 at 02:28):

I recently stumbled upon https://www.irif.fr/~sozeau/research/publications/drafts/Coq_Coq_Correct.pdf. Are there plans to replace Coq's kernel (and/or coqchk) with a verified implementation extracted from Gallina (perhaps using primitive arrays and strings?)? (Or more generally what's the current state and roadmap of this project?)

view this post on Zulip Théo Winterhalter (Sep 07 2020 at 07:26):

I'd say we're not there yet. It could be used as an external checker at some point, but before that we need to overcome one of the main issues preventing us from checking the standard library : η-expansion that we do not support yet.

view this post on Zulip Théo Winterhalter (Sep 07 2020 at 07:27):

Also for now (but probably in part because we do not use primitive structures), we are not as efficient as the current kernel.

view this post on Zulip Karl Palmskog (Sep 07 2020 at 09:19):

what I would like to see is the option to easily check Coq proofs in CI using MetaCoq's checker. This would be one extra layer of trustworthiness. One should be able to go all the way from casual check-only-affected-proofs-in-any-order-using-vio/vos/vok without bothering about universe consistency, all the way to fully checking a project end-to-end with MetaCoq, including dependencies.

view this post on Zulip Théo Winterhalter (Sep 07 2020 at 09:20):

That sounds great indeed.

view this post on Zulip Karl Palmskog (Sep 07 2020 at 09:21):

@Théo Winterhalter so are there nontrivial developments that can be checked right now that don't have η-expansion?

view this post on Zulip Karl Palmskog (Sep 07 2020 at 09:22):

or do you think successfully checking of the stdlib is the milestone needed before wider application?

view this post on Zulip Théo Winterhalter (Sep 07 2020 at 09:22):

Given that we cannot check the standard library it is a huge problem to check almost anything. We can check some HoTT library stuff but again only to some extent.

view this post on Zulip Karl Palmskog (Sep 07 2020 at 09:23):

ah, so basically not even init works? (Coq.Init.Logic)

view this post on Zulip Théo Winterhalter (Sep 07 2020 at 09:23):

It seems like it yes, this way we would be able to at least check our own checker. :)
The plan right now is to have η.

I'm not sure about init to be honest, maybe @Matthieu Sozeau has a better idea.

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 09:24):

What's the ETA of η by the way?

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 09:24):

(Pun not intended.)

view this post on Zulip Théo Winterhalter (Sep 07 2020 at 09:28):

We're having trouble on two fronts:

view this post on Zulip Karl Palmskog (Sep 07 2020 at 09:35):

@Théo Winterhalter but basically, if you solve η, there are no remaining problems in principle to check larger developments?

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 09:43):

... modules?

view this post on Zulip Karl Palmskog (Sep 07 2020 at 09:46):

hmm, there are quite large developments that don't use modules, no? But obviously one must be able to reference constants elsewhere. I don't know how deep the module system goes into everything else.

view this post on Zulip Enrico Tassi (Sep 07 2020 at 09:48):

This is true, but IIRC even arithmetic in stdlib uses them... so it is very easy to "use modules" without using them.

view this post on Zulip Théo Winterhalter (Sep 07 2020 at 09:53):

Right, we're also missing modules and template polymorphism. And now sections are part of the kernel too right? So that too.

view this post on Zulip Enrico Tassi (Sep 07 2020 at 10:01):

Sections are part of the kernel for a bad reason. IMO you should discharge the term before typing it (eliminate the section "sugar" before the term reaches the kernel).

view this post on Zulip Karl Palmskog (Sep 07 2020 at 10:01):

oh damn, no sections either. I should send an angry letter to whomever added sections to the kernel on behalf of proof engineering researchers worldwide

view this post on Zulip Karl Palmskog (Sep 07 2020 at 10:02):

(since sections are near-universally used and thus will stop a larger experimental eval of MetaCoq)

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 10:08):

@Karl Palmskog I am the culprit, but the situation before was essentially a nice backdoor into the kernel.

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 10:08):

They're not part of the checker though, so it shouldn't affect MetaCoq.

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 10:10):

It's the same trick as for the infamous "side-effects", i.e. kernel extension that matter for the performance of vo compilation but are irrelevant once you got the proof compiled.

view this post on Zulip Karl Palmskog (Sep 07 2020 at 10:10):

right, Emilio explained the basics to me. It was added in 8.12 though, right? Not in 8.11?

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 10:10):

I don't remember exactly...

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 10:11):

@Théo Winterhalter template poly is going to be fun as well, I forgot about that one :cock-a-doodle-doo:

view this post on Zulip Théo Winterhalter (Sep 07 2020 at 10:18):

Well the plan is never to include template polymorphism in MetaCoq and pressure you into removing it from the kernel. :)

view this post on Zulip Matthieu Sozeau (Sep 07 2020 at 10:19):

Modules are not a big practical issue yet, as we can still reify things inside modules. Just not the module and functor structures themselves

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 10:45):

@Théo Winterhalter the problem doesn't come from me, I'd be happy to get rid of them in the kernel as well. Two words: "backwards compatibility".

view this post on Zulip Pierre-Marie Pédrot (Sep 07 2020 at 10:46):

Also it's likely we'll have some performance issues if we get rid of template.

view this post on Zulip Théo Winterhalter (Sep 07 2020 at 11:56):

Yeah yeah, I know!


Last updated: Oct 16 2021 at 01:03 UTC