Timeline for Consequences of technically proving anything in Coq (on at least Linux) exploiting a bug? [closed]
Current License: CC BY-SA 3.0
31 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 25, 2015 at 16:01 | comment | added | joro | @JoelDavidHamkins If you are interested in this, you might consider asking something close to this. Probably fewer people will to vote close a person of your reputation ;) | |
| Mar 25, 2015 at 15:46 | comment | added | Joel David Hamkins | I had just meant that it was circulating on G+ with Richard's post. I didn't mean any big deal about "news". | |
| Mar 25, 2015 at 15:34 | comment | added | joro | @JoelDavidHamkins If "news" have few than 10^6 impressions per day, I don't consider it "current news", might be wrong on this :) | |
| Mar 25, 2015 at 15:04 | comment | added | Joel David Hamkins | Richard had just posted a link to the first link. (And you don't generally need a Google account to see G+ posts, but I notice that Richard had only shared that privately.) | |
| Mar 25, 2015 at 15:01 | comment | added | joro | @JoelDavidHamkins I don't have google account so can't see your second link. If you read the coq mailing list, you will see many bugs like the first link. One of the reasons I asked this is "computers know better", which is closely related to Technological singularity en.wikipedia.org/wiki/Technological_singularity | |
| Mar 25, 2015 at 14:22 | comment | added | Joel David Hamkins | I heard about github.com/clarus/falso from Richard Zach plus.google.com/u/0/+RichardZach/posts/CFQJQSQtmRd. | |
| Mar 25, 2015 at 14:14 | comment | added | joro | @JoelDavidHamkins Thanks. I don't care about reopening. Would you please give reference for the Coq news? (to save me search time). Btw, if you care about reopening you might consider editing the question and bumping it. | |
| Mar 25, 2015 at 13:43 | review | Reopen votes | |||
| Mar 25, 2015 at 14:50 | |||||
| Mar 25, 2015 at 13:30 | comment | added | Joel David Hamkins | I have voted to reopen. Coq bugs are in current news. | |
| Dec 28, 2011 at 14:42 | history | undeleted | François G. Dorais | ||
| Dec 21, 2011 at 18:35 | history | deleted |
Andy Putman Andrés E. Caicedo Bill Johnson |
||
| May 18, 2011 at 8:10 | comment | added | joro | homepages.inf.ed.ac.uk/rpollack/export/believing.ps.gz How to believe a machine-checked proof. In G. Sambin and J. Smith, editors, Twenty Five Years of Constructive Type Theory. Oxford Univ. Press, 1998 | |
| May 9, 2011 at 7:02 | history | edited | joro | CC BY-SA 3.0 |
Coq developers reply
|
| May 6, 2011 at 21:24 | comment | added | Mark Adams | @joro: It depends on the kind of formal logic that it's for. There are various dedicated SAT solvers (for propositional logic only), many are dedicated to first-order logics (I understand that Vampire is supposed to be amongst the best), and then those for more expressive, higher-order logics (like HOL, Isabelle, Coq and PVS). In the hands of a sufficiently expert user, all the main "higher-end" systems can be used very effectively, but the trouble is there are only a handful of "sufficiently expert" users (and I am not one!). I'm afraid I don't know which are powerful but very easy to use. | |
| May 6, 2011 at 5:57 | comment | added | joro | @Mark btw, what are the best automatic proof generators? Isabelle's sledgehammer doesn't seem very powerful. | |
| May 5, 2011 at 15:39 | comment | added | Mark Adams | @joro: Yes, you'd get a reward if you could show |- true <=> false. See the HOL Zero webpage for more info and the download. It has no warranty (it has GPL3 licence), as is usual for all software I think. It would be somewhat foolhardy to give out free software and accept warranty! Be happy with $100! | |
| May 4, 2011 at 15:35 | history | edited | joro | CC BY-SA 3.0 |
dishonest human provers
|
| May 4, 2011 at 11:56 | comment | added | Did | @unknown Hmmm... OK, thanks. Then this means I am notified of no comment at all. | |
| May 4, 2011 at 11:15 | comment | added | user9072 | @Didier Piau: Regarding your 'unrelated'. I strongly believe, the @ has no effect on this site (in contrast to some similar sites, as this one uses an older version of the underlying software). | |
| May 4, 2011 at 9:37 | history | edited | joro | CC BY-SA 3.0 |
attempt at cross-platform solution ;)
|
| May 4, 2011 at 8:06 | comment | added | Did | @Todd: Indeed. Thanks for the link. (Unrelated: maybe try to add this @ thing to your comments, I only got yours by chance.) | |
| May 3, 2011 at 22:46 | history | closed |
Todd Trimble Andrés E. Caicedo Richard Borcherds Daniel Moskovich Qiaochu Yuan |
off topic | |
| May 3, 2011 at 21:04 | comment | added | Todd Trimble | Didier: you're not the only one who thinks so. Meta thread: tea.mathoverflow.net/discussion/1037/… | |
| May 3, 2011 at 20:30 | comment | added | Did | This question amounts to a quite peculiar use of MO. | |
| May 3, 2011 at 20:15 | answer | added | Adam | timeline score: 6 | |
| May 3, 2011 at 20:11 | comment | added | Adam | While the Calculus of Constructions is certainly appropriate material for mathoverflow, this question is relevant only to one specific implementation (Coq). As such, it isn't really a math question (or even a computer science question, for that matter!). Please file a bug on the coq bug tracker. Vote to close. | |
| May 3, 2011 at 19:30 | answer | added | Andrej Bauer | timeline score: 60 | |
| May 3, 2011 at 18:00 | history | edited | joro | CC BY-SA 3.0 |
source of a.ml plugin
|
| May 3, 2011 at 15:52 | comment | added | joro | @Junkie: you mean coqc and coqchk shouldn't be trusted at all? | |
| May 3, 2011 at 15:15 | comment | added | Junkie | There is something called HOL Zero which tries to circumvent all methods of deviance. proof-technologies.com/holzero.html | |
| May 3, 2011 at 15:07 | history | asked | joro | CC BY-SA 3.0 |