Vanilla 1.1.9 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 11 of 11
What to do about this one?
Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?
I'm tempted to close --- this should just be a bug report on the coq bug tracker.
I'm also a little annoyed at the immediate crossposting with M.SE.
Well, the phrase «Hostile ocaml plugins» amused me a little, so not all is bad :)
I really don't understand the motivation behind the question. As far as I can tell, the OP is leaving things unsaid because he/she thinks they are obvious (e.g. "this is a huge problem because _______") and is coming from a very different background than mine. Are ships going to sink and airplanes going to fall out of the sky if Coq proves things that are false? (Not a rhetorical question; I really don't know.)
I also find the answer more informative than the question, but the trouble is that some influential papers in what can be seen as core topology are now being written in the hostile syntax of Coq, http://homotopytypetheory.org/links
As a type theorist, I find Coq syntax an incredibly friendly way of making certain parts of core topology much more accessible to me. :)
(I should also add that regardless of whether it is really core topology or not, HTT is first-rate work on type theory.)
I clicked through on the other answer to find the FAQ which included this gem (emphasis mine):
4 What are the other theorem provers?
Many other theorem provers are available for use nowadays. Isabelle, HOL, HOL Light, Lego, Nuprl, PVS are examples of provers that are fairly similar to Coq by the way they interact with the user. Other relatives of Coq are ACL2, Agda/Alfa, Twelf, Kiv, Mizar, NqThm, Omega...
Perhaps you have to be someone far more familiar with small children than automatic proof checkers to understand ...
1 to 11 of 11