23 events
when toggle format what by license comment
S Apr 4 '19 at 7:04 history suggested n.gaurav CC BY-SA 4.0
corrected spelling, fixed grammar
Apr 3 '19 at 11:19 review Suggested edits
S Apr 4 '19 at 7:04
Apr 13 '17 at 12:32 history edited CommunityBot
replaced http://cstheory.stackexchange.com/ with https://cstheory.stackexchange.com/
Dec 10 '16 at 15:47 comment added David Stone For the majority of programs that I spend my time working on, a proof that the program ever does halt would indicate a bug in the program. Many programs (for instance, the program that runs a pacemaker or a web server) should not halt in the typical case.
Jul 1 '16 at 6:24 answer Joshua Grochow timeline score: 5
May 27 '15 at 2:50 answer Victor Yodaiken timeline score: 1
May 26 '15 at 7:10 comment added Andrej Bauer "Provably" is misused here several times but it's not your fault. Computer scientists do it all the time. You do not mean "provably correct programs" but presumably "programs whose correctness has been proved".
Jan 19 '11 at 4:55 history tweeted twitter.com/#!/StackCSTheory/status/27589980893224960
Jan 5 '11 at 1:37 comment added Alex ten Brink @user1749: I used to believe that as well, but watch out what your reasoning proves: it proves that if a program halts on a certain input, you can prove this. However, since interesting languages are infinite, you can't prove always prove halting this way.
Jan 4 '11 at 16:54 comment added Antonio Valerio Miceli-Barone @Alex: if a program halts on a given input, then its execution trace is a proof that it halts. Hence, if a program halts, then given enough time a computer can always prove it. However, there exist programs that do not halt, and it can't be proved that that they don't halt.
Jan 2 '11 at 19:20 answer Kaveh timeline score: 22
Jan 2 '11 at 18:35 answer chazisop timeline score: 4
Jan 2 '11 at 18:23 comment added Neel Krishnaswami @Colin: that paper is worth reading for its analysis of proof, but its predictions have been falsified. Today we have provably correct compilers, operating system kernels, garbage collectors, and databases, all of which they predicted to be impossible. The trick to evade their critique was to avoid human verification of the low-level details of formal proofs, but to use machine verification of proofs, and use humans to verify the proof checker. Noam's ref to type theory is where the state of the art is, which leaves imperative programs in something of a bind since type theory is functional.
Jan 2 '11 at 16:48 comment added Alex ten Brink @Colin, I read the paper you linked. While it was an interesting read and posed a number of valid points, I was surprised by the adversarial tone of the paper.
Jan 2 '11 at 16:24 comment added Radu GRIGore Program verification is undecidable. So one problem is to say what constitutes a good solution. See cstheory.stackexchange.com/questions/4016/…
Jan 2 '11 at 12:36 answer Noam Zeilberger timeline score: 18
Jan 2 '11 at 11:56 comment added Colin McQuillan On the first question, an influential paper is "Social processes and proofs of theorems and programs", portal.acm.org/citation.cfm?id=359106
Jan 2 '11 at 9:45 answer Radu GRIGore timeline score: 12
Jan 1 '11 at 22:33 answer Neel Krishnaswami timeline score: 28
Jan 1 '11 at 21:39 comment added Mark Reitblatt I think you should split them up. They are different questions with different answers.
Jan 1 '11 at 18:17 comment added Alex ten Brink A compiler could enumerate all possible proofs of length i, letting i go from 1 to infinity, until it finds a proof that the program halts. If we require that the input for the compiler provably halts, then the compiler will always find that proof. Since the halting problem is undecidable, we must conclude there are programs that halt, but no proof for this exists. The crucial point is that programs are unable to find out if a proof exists, not that they are unable to find a proof if it exists.
Jan 1 '11 at 16:57 comment added Alex ten Brink I realise I asked two questions that are essentially in two different fields in CS. Since they are closely related, I decide to go with a single question, but I could of course split them up if the powers that be think that is a better idea.
Jan 1 '11 at 16:56 history asked Alex ten Brink CC BY-SA 2.5