# Timeline for What do we know about provably correct programs?

### Current License: CC BY-SA 2.5

7 events
when toggle format what by license comment
Apr 13 '17 at 12:32 history edited CommunityBot
replaced http://cstheory.stackexchange.com/ with https://cstheory.stackexchange.com/
Jan 3 '11 at 6:27 comment Andrej Bauer has a new interesting post on his blog in which he proves Godel's Dialectica Interpretation in Coq.
Jan 2 '11 at 22:33 history edited
Jan 2 '11 at 22:10 comment @Radu: thanks for pointing out that it can be done automatically in Coq. As you mentioned one can also extract some constructive information and therefore programs from classical proofs of theorem using proof mining for some classes of formulas (interested people can check Ulrich Kuhlenbach's papers for details). Another possibly related result is that if a $\Pi^0_2$ theorem is proven in $PA$, it is also provable constructively in $HA$ by Harvey Friedman's translation. _