Stream: Coq users

Topic: Program extraction plans


view this post on Zulip Huỳnh Trần Khanh (Nov 23 2023 at 03:23):

Here's a message posted on the /r/ProgrammingLanguages Discord server:

I'm also will be going with lean. Coq is unappealing because it doesn't seem you can make proper programs in it. You either have to program in a different language, define its semantics in coq and prove the correctness of the program, or you have some coq extractor feature that looks nice on paper but people keep telling me it sucks in practice

With lean you just go and make your thing

Do we have plans to improve the program extraction system to attract users? I feel the threat of Lean eclipsing Coq is getting more and more real.

view this post on Zulip Théo Winterhalter (Nov 23 2023 at 11:51):

With lean you just go and make your thing

What does that mean?

view this post on Zulip Karl Palmskog (Nov 23 2023 at 11:58):

proved extraction is mentioned in the Coq Roadmap: https://github.com/coq/ceps/blob/coq-roadmap/text/069-coq-roadmap.md#proved-extraction (and is to my knowledge worked on here)

There are already many large Coq extraction based projects in the legacy extraction pipeline for OCaml and Haskell, and Dune has pretty good support for integrating extraction of OCaml into builds. The trusted computing base (TCB) for current extraction is unsatisfactory, but at least quite well studied (OCaml Obj.magic and the like).

Is there a breakdown of the TCB for running Lean programs? My impression is that without running a checker post-hoc on terms stored in files, Lean gives very few guarantees about any results (due to input/output, etc.)

view this post on Zulip Karl Palmskog (Nov 23 2023 at 11:59):

maybe this would be a good opportunity to ask @Bas Spitters about the status of Certicoq, I know it's at least used here for verified WebAssembly.

view this post on Zulip Huỳnh Trần Khanh (Nov 23 2023 at 12:11):

Right here: https://softwarefoundations.cis.upenn.edu/vfa-current/Extract.html

The section "Lightweight Extraction to int" mentions a very important problem. On the Lean side, there's no such dance. Lean uses GMP.

view this post on Zulip Huỳnh Trần Khanh (Nov 23 2023 at 12:12):

Yes, the trusted computing base is bigger. But then again, using GMP isn't the biggest threat to soundness. It's a battle tested library.

view this post on Zulip Théo Winterhalter (Nov 23 2023 at 12:12):

Isn't that what primitive ints are for though?

view this post on Zulip Karl Palmskog (Nov 23 2023 at 12:15):

yes, Coq already supports extraction to primitive ints (ExtrOCamlInt63), and the code for using this in a separate project is available in Coq's GitHub repo. I have a proposed packaging here of this code, which I hope to integrate into Coq for the 8.20 cycle: https://github.com/palmskog/coq-primitive

view this post on Zulip Karl Palmskog (Nov 23 2023 at 12:16):

for example, there is this refinement of MathComp's ints to primitive ints, but it will have to be reimplemented for use in the wider community since it's under a noncommercial license: https://gitlab.com/formalv/formalv/-/tree/dev/theories/prim63_mathcomp

view this post on Zulip Bas Spitters (Nov 23 2023 at 13:02):

More information on our wasm backend here: https://www.cl.cam.ac.uk/~jp622/certicoq-wasm.pdf
For the general status of certicoq, one should problem ask @Yannick Forster or @Matthieu Sozeau

view this post on Zulip Karl Palmskog (Nov 23 2023 at 13:05):

but is the CertiCoq-WASM work end-to-end verified (modulo parsing)? Last I looked at the CertiCoq wiki, there were missing pieces in the "full" compilation/translation proofs

view this post on Zulip Karl Palmskog (Nov 23 2023 at 13:07):

anyway, I think it shows that some significant pieces of CertiCoq can be reused right now, even if the full end-to-end guarantees for CertiCoq itself are not Qed'd yet

view this post on Zulip Yannick Forster (Nov 23 2023 at 13:09):

There is no end-to-end theorem for CertiCoq yet. I think there could be an end-to-end theorem using CPS translation, but the current goal is to obtain an end-to-end theorem by verifying the ANF translation ( @Zoe Paraskevopoulou is working on that) and then hopefully we can compose the theorem (which, as we learned in the project of verified extraction to OCaml / Malfunction, is very much non-trivial to get)

view this post on Zulip Yannick Forster (Nov 23 2023 at 13:09):

But yes, all pieces of CertiCoq are reusable already - I think that's what Bas and colleagues are doing

view this post on Zulip Yannick Forster (Nov 23 2023 at 13:10):

For extraction to OCaml / Malfunction we do have an end-to-end theorem since recently, the next step is to work on the user interface and some unverified features to make it more accessible / integrate it into Coq

view this post on Zulip Huỳnh Trần Khanh (Nov 23 2023 at 13:14):

it's great that you're working on WASM extraction. however, not having garbage collection is a tough sell. WASM recently has a high level garbage collection API, you should look into integrating it

view this post on Zulip Karl Palmskog (Nov 23 2023 at 13:27):

it's not obvious to me that Coq should be the general programming language that Lean seems to be aiming for, with built-in I/O by default and so on. But it's worth organizing and flagging up the many optional pipelines for programming and verification in Coq, not least in the Platform (e.g., coq-simple-io gives I/O monad)

view this post on Zulip Bas Spitters (Nov 23 2023 at 13:49):

@Yannick Forster What do you mean no end-to-end? We go from /-ANF to wasm and that part has been verified.
There are some limitations, as mentioned in the abstract above.

view this post on Zulip Yannick Forster (Nov 23 2023 at 13:51):

end-to-end as in a theorem talking about the relation between a Coq program and its translation to WASM

view this post on Zulip Yannick Forster (Nov 23 2023 at 13:51):

/ for CertiCoq, a theorem talking about the relation between a Coq program and its translation to C

view this post on Zulip Karl Palmskog (Nov 23 2023 at 13:52):

but the ideal should be: the relation between a Coq function and its translation to machine code for a specific ISA - right?

Or even further to program execution on hardware that implements a specific ISA.

view this post on Zulip Karl Palmskog (Nov 23 2023 at 13:55):

(but yes, those end-to-end proofs will require CompCert, so dependency issues I guess)

view this post on Zulip Huỳnh Trần Khanh (Nov 23 2023 at 14:08):

I do feel like Coq should be a general purpose language. or there should be a Coq plugin that transforms Coq into a general purpose language. of course this isn't gonna be useful for every single use case, for example Lean programming facilities are utterly useless for my use case because competitive programming problems have tight performance constraints. you know it's just kinda awesome when you can tell a senior backend dev that you can straight up write a verified HTTP server in Coq

view this post on Zulip Huỳnh Trần Khanh (Nov 23 2023 at 14:11):

btw where's the certicoq-wasm source code

view this post on Zulip Huỳnh Trần Khanh (Nov 23 2023 at 14:13):

I feel patching the project to use wasm-gc might be a worthwhile thing

view this post on Zulip Karl Palmskog (Nov 23 2023 at 14:57):

there was already some work on verified HTTP servers, but I think it reinforces that Coq is not going to be a language one just opens up and hacks together a user-facing application in

view this post on Zulip Michael Soegtrop (Nov 23 2023 at 15:01):

I remember a development from the MIT where they also verified the HW (except for the network card), but I can't find the reference right now.

view this post on Zulip Karl Palmskog (Nov 23 2023 at 15:02):

http://adam.chlipala.net/papers/LightbulbPLDI21/LightbulbPLDI21.pdf


Last updated: Jun 22 2024 at 16:02 UTC