Stream: Coq workshop 2020

Topic: [M] Invited Talk

Emilio Jesús Gallego Arias (Jun 30 2020 at 20:57):

This is the topic to ask questions for the Invited Talk: "A Coq retrospective, at the heart of Coq architecture, the genesis of version 7.0" by
Jean-Christophe Filliâtre

Emilio Jesús Gallego Arias (Jul 06 2020 at 09:06):

Invited talk will start at 11:30

Maxime Dénès (Jul 06 2020 at 09:46):

So, in Coq 7, we had exactly type safe_env = env?

Maxime Dénès (Jul 06 2020 at 09:47):

Today:

type safe_environment =
  { env : Environ.env;
    sections : section_data Section.t option;
    modpath : ModPath.t;
    modvariant : modvariant;
    modresolver : Mod_subst.delta_resolver;
    paramresolver : Mod_subst.delta_resolver;
    revstruct : structure_body;
    modlabels : Label.Set.t;
    objlabels : Label.Set.t;
    univ : Univ.ContextSet.t;
    future_cst : Univ.ContextSet.t Future.computation list;
    engagement : engagement option;
    required : vodigest DPmap.t;
    loads : (ModPath.t * module_body) list;
    local_retroknowledge : Retroknowledge.action list;
}

Hugo Herbelin (Jul 06 2020 at 09:47):

IIRC, yes

Hugo Herbelin (Jul 06 2020 at 09:47):

This changed with the introduction of modules, IIRC

Chantal Keller (Jul 06 2020 at 09:48):

I have a question more for current Coq developers: which ideas are still present in the kernel? (more informally than what Maxime just posted)

Pierre Corbineau (Jul 06 2020 at 09:48):

About the abstraction barrier : was HOL/HOL light an inspiration on the design of the kernel?

Gaëtan Gilbert (Jul 06 2020 at 09:49):

Maxime Dénès said:

So, in Coq 7, we had exactly type safe_env = env?

https://github.com/coq/coq/commit/12965209478bd99dfbe57f07d5b525e51b903f22

+type safe_environment =
+    { old : safe_environment;
+      env : env;
+      modinfo : module_info;
+      labset : Labset.t;
+      revsign : module_signature_body;
+      revstruct : module_structure_body;
+      imports : library_info list;
+      loads : (module_path * module_body) list }

-type safe_environment = env

Karl Palmskog (Jul 06 2020 at 09:50):

do you think it would be worthwhile to verify (e.g., in Coq ) any other parts of a proof assistant than its kernel/core, for example, a rollback mechanism or file system interaction? diminishing returns?

Emilio Jesús Gallego Arias (Jul 06 2020 at 09:50):

@Jean-Christophe Filliâtre did you consider the kernel to be extensible [in terms of different Type Theories] , do you have any comments on whether that's a good idea, interface, ...

Maxime Dénès (Jul 06 2020 at 09:51):

Q: How would you make sure a more defensive kernel API would not be too costly (e.g. when called from tactics)?

Karl Palmskog (Jul 06 2020 at 09:52):

do you think the Coq and Why3 program verification approaches will ever be unified? Should they be?

Maxime Dénès (Jul 06 2020 at 09:55):

Q: Were you tempted to use object-oriented features sometimes? E.g. for the registration mechanism, it may seem natural to see data bundled with their save/restore functions.

Chantal Keller (Jul 06 2020 at 09:56):

thanks!

Enrico Tassi (Jul 06 2020 at 09:57):

Thanks for the nice talk!

Emilio Jesús Gallego Arias (Jul 06 2020 at 10:00):

For this kind of project, how did you find OCaml? Are there any features that would make your life easier?

Maxime Dénès (Jul 06 2020 at 10:02):

Thanks a lot for your answers!

Emilio Jesús Gallego Arias (Jul 06 2020 at 10:02):

Actually OCaml developers asked that question to us

Pierre-Marie Pédrot (Jul 06 2020 at 10:03):

Wouldn't you use Rust instead today?

Emilio Jesús Gallego Arias (Jul 06 2020 at 10:05):

Thanks a lot @Jean-Christophe Filliâtre !

Pierre Corbineau (Jul 06 2020 at 10:05):

thanks a lot for the talk and answers!

Michael Soegtrop (Jul 06 2020 at 10:06):

Thanks, a very nice talk!

Karl Palmskog (Jul 06 2020 at 10:06):

@Jean-Christophe Filliâtre a request on behalf of the proof assistant research community: could you put your Coq 7.0 tech report ("Design of a proof assistant: Coq version 7") on a permanent archive such as HAL for ease of citation/access? This report is one of very few publications on proof assistant implementation design.

Jean-Christophe Filliâtre (Jul 06 2020 at 10:08):

Let me do that right now :-)

Jean-Christophe Filliâtre (Jul 06 2020 at 10:16):

Done: https://hal.inria.fr/hal-02890416

Karl Palmskog (Jul 06 2020 at 10:22):

@Théo Zimmermann @Emilio Jesús Gallego Arias perhaps you could link the report (when it appears on HAL) next to the talk info on the workshop website ?

Emilio Jesús Gallego Arias (Jul 06 2020 at 10:23):

very good idea, thanks @Karl Palmskog !

Last updated: Sep 15 2024 at 12:01 UTC