Timeline for Halting problem theory vs. practice
Current License: CC BY-SA 4.0
20 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 2, 2020 at 16:11 | answer | added | Rexcirus | timeline score: 0 | |
| Jun 10, 2020 at 7:33 | comment | added | Raphael | I seem to remember quite a few older questions on the site about this very issue. | |
| Jun 6, 2020 at 10:37 | answer | added | gnasher729 | timeline score: 0 | |
| Jun 5, 2020 at 21:59 | comment | added | Moshe Vardi | For a discussion of this issue, see Solving the Unsolvable. There is also the May 2011 issue of Communications included an article by Byron Cook, Andreas Podelski, and Andrey Rybalchenko, titled "Proving Program Termination" (p. 88), in which they argued that "in contrast to popular belief, proving termination is not always impossible." | |
| Jun 5, 2020 at 13:35 | answer | added | Hugo Sereno Ferreira | timeline score: 2 | |
| Jun 5, 2020 at 11:37 | answer | added | RogerS | timeline score: 1 | |
| May 13, 2020 at 17:12 | vote | accept | Jack Fleming | ||
| May 12, 2020 at 23:08 | comment | added | slebetman | Yes, HTML guarantees halting. Also regular expression (not PCRE - PCRE is Turing-complete, not regular) | |
| May 12, 2020 at 20:49 | comment | added | Martin Frodl | Obligatory xkcd: xkcd.com/1266 | |
| May 12, 2020 at 16:38 | comment | added | user21820 |
@PabloH: I think you're saying exactly the same thing as I did. =) A general-purpose programming language that allows termination proofs can do so via both static verification (such as for a restricted sublanguage) and human-assisted verification. Off-topic, but I always found Java's final keyword slightly annoying because it did not prevent performing operations on that final object, which means that immutable data structures implemented as generic classes are only immutable if the inputs are themselves immutable.
|
|
| May 12, 2020 at 16:31 | comment | added | Pablo H |
@user21820 I think it's useful to have total code, total functions, a total sub-language, so that you can concentrate on the rest. In the same way you have const, final, notnull, etc. keywords to restrict your code. Restricted is good (for the particular tasks that can be implemented, of course). :-)
|
|
| May 12, 2020 at 15:32 | answer | added | PMar | timeline score: 1 | |
| May 12, 2020 at 10:58 | comment | added | IS4 | Well, one could say that in practice, every program terminates as it eventually runs out of space or time. | |
| May 12, 2020 at 10:13 | comment | added | Polygnome | A related, and also interesting (and limiting) theorem: Rice's Theorem | |
| May 12, 2020 at 7:34 | comment | added | user21820 | You don't need the programming language to force totality of the program. What you need for mission-critical code is a sufficiently simple programming language coupled with a proof verifier, where you can provide a proof of termination that can be verified. Programming languages that only allow total programs would be just a very restrictive kind (i.e. no termination proof required). But it is far more useful to have a general-purpose programming language that allows human proofs of program termination. Such programming languages and verifiers do exist, but I am not an expert in this. | |
| May 12, 2020 at 4:29 | history | became hot network question | |||
| May 11, 2020 at 21:48 | history | edited | Jake |
added tags
|
|
| May 11, 2020 at 21:47 | answer | added | Jake | timeline score: 20 | |
| May 11, 2020 at 20:30 | review | First posts | |||
| May 12, 2020 at 4:05 | |||||
| May 11, 2020 at 20:25 | history | asked | Jack Fleming | CC BY-SA 4.0 |