tea.mathoverflow.net - Discussion Feed (Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?)

an_mo_user comments on "Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?" (14404)

an_mo_user — Wed, 04 May 2011 04:23:14 -0700

Sorry for going super off-topic now:
I was under the impression that Lego (not the proof-checker) is essentially universally known.
Is this just a more local thing than I thought (I am not too far away from Denmark so...)?
Or did I miss a more subtle point.

Andrew Stacey comments on "Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?" (14403)

Andrew Stacey — Wed, 04 May 2011 04:13:22 -0700

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

neelk comments on "Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?" (14402)

neelk — Wed, 04 May 2011 02:31:43 -0700

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

darijgrinberg comments on "Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?" (14400)

darijgrinberg — Wed, 04 May 2011 00:12:46 -0700

I think the problem is that the OP is considering Coq as a security system, while it really is a safety system. But of course, if people start misusing it as a former in future (a misconception that seems hard to avoid, given the "100% sure" clichée of mathematical proof that most of the populace has), questions like this will become way more urgent, and I am pretty sure somebody will find much simpler attacks than the one shown in the OP.

Kevin Buzzard comments on "Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?" (14399)

Kevin Buzzard — Wed, 04 May 2011 00:00:52 -0700

Sergey: I guess you are saying "if Coq proves something false then this might be because ZF proves something false". That's true, but I don't think one can deduce from this that "if Coq proves something false then it is worth talking about on MO" because there might be other far more mundane reasons.

The MO thread as it currently stands simply says "if you put garbage in to a computer program then you get garbage out". One can philosophise about other reasons for getting garbage out but I don't think that justifies the existence of the MO question.

Sergey Melikhov comments on "Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?" (14397)

Sergey Melikhov — Tue, 03 May 2011 18:42:13 -0700

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

@Qiaochu Yuan: Depending on why that would happen with Coq, it might be worse (or more interesting) than ZFC proving things that are false: see the above link and http://www.jstor.org/pss/20118649

So perhaps the question itself ("What are the consequences of technically proving anything in Coq?") is just as legitimate as those on potential contradictions in ZFC or on false proofs of e.g. the Riemann hypothesis. Of course it would read smoother if the Coq code was replaced by a human-readable explanation.

Qiaochu Yuan comments on "Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?" (14395)

Qiaochu Yuan — Tue, 03 May 2011 15:49:50 -0700

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

an_mo_user comments on "Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?" (14394)

an_mo_user — Tue, 03 May 2011 15:35:24 -0700

Not to forget the radioactive banana in the answer!

But, kidding aside, I found the answer not only funny but also informative and am happy it was given (and possible to give it, i.e. not closed).

Mariano comments on "Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?" (14392)

Mariano — Tue, 03 May 2011 14:07:20 -0700

Well, the phrase «Hostile ocaml plugins» amused me a little, so not all is bad :)

Scott Morrison comments on "Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?" (14391)

Scott Morrison — Tue, 03 May 2011 13:59:24 -0700

I'm also a little annoyed at the immediate crossposting with M.SE.

Scott Morrison comments on "Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?" (14390)

Scott Morrison — Tue, 03 May 2011 13:59:10 -0700

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.