Timeline for On proof-verification using Coq
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Nov 12, 2018 at 0:14 | history | suggested | jeq | CC BY-SA 4.0 |
Corrected some English typos.
|
| Nov 11, 2018 at 23:02 | review | Suggested edits | |||
| S Nov 12, 2018 at 0:14 | |||||
| Nov 11, 2018 at 19:15 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
added 599 characters in body
|
| Nov 11, 2018 at 19:07 | comment | added | Andrej Bauer | Ah, I misunderstood the question. I will supplement the answer. | |
| Nov 11, 2018 at 18:01 | comment | added | Timothy Chow | Great answer. But I think that Question 2 was asking about computer runtime, not programming person-hours. For most "ordinary" proofs of "ordinary" theorems the running time is essentially instantaneous. However, there can be exceptions, e.g., Flyspeck. If part of the proof is a huge computer calculation, then Coq may have to rerun the entire computation, and it will be a lot slower than if you simply programmed it in C, since Coq has to verify the formal correctness of every step of the computation. | |
| S Nov 11, 2018 at 16:25 | history | suggested | Josiah Park | CC BY-SA 4.0 |
typo/ redundant articles removed
|
| Nov 11, 2018 at 14:54 | review | Suggested edits | |||
| S Nov 11, 2018 at 16:25 | |||||
| Nov 11, 2018 at 10:52 | history | answered | Andrej Bauer | CC BY-SA 4.0 |