Stream: Coq devs & plugin devs

Topic: Verified Kernel

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

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.

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.

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.

Théo Winterhalter (Sep 07 2020 at 09:20):

That sounds great indeed.

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?

Karl Palmskog (Sep 07 2020 at 09:22):

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

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.

Karl Palmskog (Sep 07 2020 at 09:23):

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

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.

Pierre-Marie Pédrot (Sep 07 2020 at 09:24):

What's the ETA of η by the way?

Pierre-Marie Pédrot (Sep 07 2020 at 09:24):

(Pun not intended.)

Théo Winterhalter (Sep 07 2020 at 09:28):

We're having trouble on two fronts:

• The best way to specify η given that we are in an untyped setting;
• How to adapt the order for proving termination of type checking.

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?

Pierre-Marie Pédrot (Sep 07 2020 at 09:43):

... modules?

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.

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.

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.

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

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

Karl Palmskog (Sep 07 2020 at 10:02):

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

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.

Pierre-Marie Pédrot (Sep 07 2020 at 10:08):

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

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.

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?

Pierre-Marie Pédrot (Sep 07 2020 at 10:10):

I don't remember exactly...

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:

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

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

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

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.

Théo Winterhalter (Sep 07 2020 at 11:56):

Yeah yeah, I know!

Last updated: Oct 12 2024 at 13:01 UTC