Stream: Coq workshop 2020

Topic: [M] Invited Talk


view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 09:06):

Invited talk will start at 11:30

view this post on Zulip Maxime Dénès (Jul 06 2020 at 09:46):

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

view this post on Zulip 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;
}

view this post on Zulip Hugo Herbelin (Jul 06 2020 at 09:47):

IIRC, yes

view this post on Zulip Hugo Herbelin (Jul 06 2020 at 09:47):

This changed with the introduction of modules, IIRC

view this post on Zulip 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)

view this post on Zulip Pierre Corbineau (Jul 06 2020 at 09:48):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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, ...

view this post on Zulip 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)?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Chantal Keller (Jul 06 2020 at 09:56):

thanks!

view this post on Zulip Enrico Tassi (Jul 06 2020 at 09:57):

Thanks for the nice talk!

view this post on Zulip 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?

view this post on Zulip Maxime Dénès (Jul 06 2020 at 10:02):

Thanks a lot for your answers!

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 10:02):

Actually OCaml developers asked that question to us

view this post on Zulip Pierre-Marie Pédrot (Jul 06 2020 at 10:03):

Wouldn't you use Rust instead today?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 10:05):

Thanks a lot @Jean-Christophe Filliâtre !

view this post on Zulip Pierre Corbineau (Jul 06 2020 at 10:05):

thanks a lot for the talk and answers!

view this post on Zulip Michael Soegtrop (Jul 06 2020 at 10:06):

Thanks, a very nice talk!

view this post on Zulip 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.

view this post on Zulip Jean-Christophe Filliâtre (Jul 06 2020 at 10:08):

Let me do that right now :-)

view this post on Zulip Jean-Christophe Filliâtre (Jul 06 2020 at 10:16):

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

view this post on Zulip 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 ?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 10:23):

very good idea, thanks @Karl Palmskog !


Last updated: Feb 06 2023 at 05:03 UTC