Timeline for Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug?
Current License: CC BY-SA 3.0
2 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 4, 2011 at 18:28 | comment | added | Mark Adams | It's good that the Coq FAQ has this list of 5 things that you trust when using Coq, but where in this list is the vulnerability highlighted above by joro? It's not really covered by the second item, "The Coq kernel implementation", because this only talks about mirroring the logic... | |
| May 3, 2011 at 20:15 | history | answered | Adam | CC BY-SA 3.0 |