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.

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’ve always been a bit interested in playing around with the language but I don’t really know what the use of the proofs are if the implementations can diverge from the proofs.

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 nat type. 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 on nat.

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.

can one actually generate running code from Coq? I’ve never quite understood how one writes programs in the conventional sense with 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

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:

So most usage of Coq is really about writing proofs?

I’ve always been a bit interested in playing around with the language but I don’t really know what the use of the proofs are if the implementations can diverge from the 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

hardto extract a code in a safe and efficient manner. For instance, just consider the`nat`

type. 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 on`nat`

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