-
can one actually generate running code from Coq? I’ve never quite understood how one writes programs in the conventional sense with Coq.
-
can one actually generate running code from Coq?
You can extract Haskell or OCaml programs from Coq:
https://coq.inria.fr/refman/Reference-Manual026.html
This was done for example when XMonad was partially verified using Coq:
https://github.com/wouter-swierstra/xmonad
I’ve never quite understood how one writes programs in the conventional sense with Coq.
Most of the time you don’t really. Proof extraction doesn’t always result in the best code. Sometimes there’s performance problems or integration problems. It’s possible, but Coq is often used to prove code then it’s ported to other platforms.
Maybe this will change in the future. Some recent ideas are going around at the moment:
In addition to using Conal’s work in Haskell, I’m also working on a Coq rendering of his idea, which I hope will give me a more principled way to extract Coq programs into Haskell, by way of their categorical representation.
-
-
So most usage of Coq is really about writing proofs?
I’d say so IMO. It’s been almost a decade but a huge breakthrough for Coq in the 2000s was Gonthier’s proof of the four color theorem in 2004. Many regard this as the most readable version proof of the four color theorem, even though it still requires trusting a computer to validate 663 cases.
People talk about validating the classification of finite abelian groups as one of the long term goals of this stuff, since the shear length of the proof makes some mathematicians wonder about its correctness.
A lot of people are attracted to Coq because of its use of dependent type theory. Idris may provide a compelling alternative, however it may not be as mature as a proof assistant.
Personally, I use a proof assistant in my spare time to explore some of my ideas in mathematics. I use Isabelle/HOL rather than Coq. This is because I’ve found Isabelle/HOL has syntax closer to conventional mathematics than Coq, which makes adapting arguments from papers and books easier for me. It also has more convenience features for non-constructive proofs than Coq last time I checked, as well as better integration with third party theorem proves like E and Z3 which makes it easier to quickly find automated proofs.
Exploring proofs in pure mathematics is all the utility I’ve found for computer proof assistants. If you are trying to solve an obscure integral or deal with symbolic z-transforms and their roots, I’ve had more luck with Mathematica. Whenever I try code generation for anything, I write unit tests. For real world correctness I think you are best served by generative testing and finding simple mathematical invariants to check (ie. left-right inverse functions).
That being said, if you love Aigner et al.’s Proofs From the Book, programming and trying out your own proofs then a computer proof assistant can be fun.
-
Coq has a feature call the code extraction. Basically, all the Prop world goes away while the Gallina code is turned into either Ocaml, Haskell or Scheme. The one important thing to know is the extraction algorithm is not itself certified. There is no equivalence proof (similar to CompCert one) between the Coq semantic and the Ocaml semantic for instance.
So, the extractor is part of the TCB and, indeed, the proof link is broken between the “model” and the “concrete machine”. However, one can argue it raises the level of confidence anyway.
One thing to know and which Coq manuals and tutorials never stress out (imo) is that the code extraction is not straightforward. It is hard to extract a code in a safe and efficient manner. For instance, just consider the
nattype. You really do not want to use the nat type in most of your program because it is highly inefficient. Yet, all the algorithmic proofs you can do in Coq have a great chance to rely onnat.Also, having a readable extracted code is not that simple. Most of the time, it goes well. But sometimes, not so much. For instance, I had some trouble with dependent type, once.
-
-
-
-
8 Validities You NEED to Become a Semilattice
- ⊢Φ⊑Φ
- ⊢Φ⊑Ψ→Ψ⊑Λ→Φ⊑Λ
- ⊢Φ⊓Ψ⊑Φ
- ⊢Ψ⊓Φ⊑Φ
- ⊢Φ⊑Φ⊔Ψ
- ⊢Φ⊑Ψ⊔Φ
- ⊢Φ⊑Λ→Ψ⊑Λ→Φ⊔Ψ⊑Λ
- ⊢Λ⊑Φ→Λ⊑Ψ→Λ⊑Φ⊓Ψ
(also, the positive implicational calculus)
-
This is a pretty sad story, for several reasons:
Java has a builtin
PriorityQueue, which you can use in Clojure if you want. It’s mutable, but it’s really easy…In the real world, Fibonacci heaps only give you a marginal speedup over binary heaps (see this stack overflow). With two hundred nodes in a dense graph, its unlikely that there’d be any noticeable difference.
For such a small graph, the offline O(N2) algorithm which computes the shortest paths for every node to every other node seems attractive.
The standard reference for functional data structures suitable for Clojure is Chris Okasaki’s 1996 thesis Purely Functional Data Structures. He implements pure, functional binary heaps in that in Standard ML. In that same year, Okasaki has also published an asymptotically optimal heap with the same complexity as Tarjan’s Fibonacci Heap. This probably would have helped the author avoid her “OMG How do I do mutable data structures in Clojure??” moment (she also could have resorted to atoms if she was desperate, or java interop if she was super-desperate).
-
i read this as a pretty happy story - at the cost of a few days of work, the author gained a deeper understanding of fibonacci heaps, persistent data structures and the tradeoffs they make. all in all i’d call it a win and i’m pretty sure she does too, despite the “ruins my life” (which i read as humorously over-the-top)
-
As a story of exploring algorithms and data structures, I found it a fascinating exploration. Often times, this is how I learn new things: might try to explore how a data structure or algorithm might be relevant to a project, even if it’s not the best, in order to better understand it and maybe get a feel for when it would be appropriate.
-
-
I don’t think the point of the project was a Fibonacci heap deliverable. The point was to learn about an interesting data structure in an interesting language. If I’m not mistaken, the author was participating in Hacker School, which has given rise to such interesting things as: http://jvns.ca/projects/#os-rust which I followed as she was writing it. Despite having taken an OS class already, this was a very interesting review of some topics we didn’t cover.
-
-
Ah, thanks for the correction! Edited above.
-
-
I feel the Isabelle/HOL tutorial is worth mentioning in this list: https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016-1/doc/tutorial.pdf
Thanks for the link to the tutorial! Although I don’t add any tutorials to the list because it’s a first source of knowledge if you want to learn tool or program and tutorials are always free so everyone can easily find.