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.

With lean you just go and make your thing

What does that mean?

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

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.

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.

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.

Isn't that what primitive ints are for though?

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

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

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

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

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

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)

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

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

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

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)

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

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

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

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.

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

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

btw where's the certicoq-wasm source code

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

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

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.

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

Last updated: Oct 13 2024 at 01:02 UTC