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?)
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.
Also for now (but probably in part because we do not use primitive structures), we are not as efficient as the current kernel.
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.
That sounds great indeed.
@Théo Winterhalter so are there nontrivial developments that can be checked right now that don't have η-expansion?
or do you think successfully checking of the stdlib is the milestone needed before wider application?
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.
ah, so basically not even
init works? (Coq.Init.Logic)
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.
What's the ETA of η by the way?
(Pun not intended.)
We're having trouble on two fronts:
@Théo Winterhalter but basically, if you solve η, there are no remaining problems in principle to check larger developments?
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.
This is true, but IIRC even arithmetic in stdlib uses them... so it is very easy to "use modules" without using them.
Right, we're also missing modules and template polymorphism. And now sections are part of the kernel too right? So that too.
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).
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
(since sections are near-universally used and thus will stop a larger experimental eval of MetaCoq)
@Karl Palmskog I am the culprit, but the situation before was essentially a nice backdoor into the kernel.
They're not part of the checker though, so it shouldn't affect MetaCoq.
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.
right, Emilio explained the basics to me. It was added in 8.12 though, right? Not in 8.11?
I don't remember exactly...
@Théo Winterhalter template poly is going to be fun as well, I forgot about that one :cock-a-doodle-doo:
Well the plan is never to include template polymorphism in MetaCoq and pressure you into removing it from the kernel. :)
Modules are not a big practical issue yet, as we can still reify things inside modules. Just not the module and functor structures themselves
@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".
Also it's likely we'll have some performance issues if we get rid of template.
Yeah yeah, I know!
Last updated: Dec 01 2023 at 07:01 UTC