15 ms·

Rice’s Theorem: An interactive tutorial

184 points by lispybanana 4y ago

DarkmSparks 4y ago
Detecting infinite loops (halting) isn't the impossible problem turing "proved" from my experience. Its just a lim/tends to problem. Which depends entirely on how you define infinity.
- tgv 4y ago
  It's not possible to write an algorithm that will detect infinite loops in all programs. But of course there are instances that can be detected, such as for () {}
  - DarkmSparks 4y ago
    As I say, from my experience that depends how and if you define infinitely. If infinite is formally defined then detecting if any function equals or tends to it is fairly trivial. quick and useful defs are "can exceed a time limit", or "can exceed the error bounds of floating point math" I'd guess you can do it formally by catching the 6 or 7 definitions of infinite, but I've never come close to needing to go that far, for most, just programatically constructing a graph of the logic and detecting infinite loops in it has proved more than sufficient.
    - UncleMeat 4y ago
      Good news. Turing defined a nonterminating Turing Machine in his paper so we don't need to worry about some weird nonstandard definition of nontermination. "Oh, computers have finite memory so actually they are finite state machines" is just needless pedantry that is not useful for the actual mathematical relevance of Turing's proof and its consequences. Yes, the field of static analysis makes practical (though not flawless) solutions to undecidable problems every day. This is not relevant here.
      - insanitybit 4y ago
        damn this Turing guy sounds like he really knew what he was talking about
      - maweki 4y ago
        The great thing about undecidable problems is, that you can put an arbitrary amount of research in and you'll probably find another subclass of instances for which the problem is indeed decidable. Only an infinite number of subclasses of instances to go. That's proven job safety for computer science researchers.
        wizeman 4y ago
        > Only an infinite number of subclasses of instances to go. There's only one subclass of instances for which the problem is undecidable: those where the program being analyzed is allowed to consume infinite memory. Which is not the same thing as saying that the program is implemented in a Turing-complete language. Because you can write a program in a Turing-complete language and yet, run it on a machine with finite memory (i.e. a computer).
      - DarkmSparks 4y ago
        nope, nothing to do with finite memory or accuracy. Thats just an easy/practical way to define it if you have a halting problem to solve. Everything to do with https://en.m.wikipedia.org/wiki/1/2_%2B_1/4_%2B_1/8_%2B_1/16_%2B_%E2%8B%AF https://en.m.wikipedia.org/wiki/1/2_%2B_1/4_%2B_1/8_%2B_1/16... halting exactly at infinity (and knowing it without summing infinitely).
        CaptainNegative 4y ago
        If one is willing to be that vague in drawing connections, one can reduce nearly every problem to any other one. But Turing was a mathematician, and very precise with his definitions (albeit not quite as pedantic as some successors such as Aho/Ullman decades later). The interesting bit about Turing's result is that it can be adapted to a wide class of mathematical and real objects. Physical systems? Yep. Time and/or space bounded machines? You bet. Actually, at its core Turing's result is itself an adaptation of Gödel's, who more broadly talks about the context of first-order mathematical theories. If one want to bring these concepts to practice (where by practice I mean the realm of proving results in theoretical cs), it's a lot more effort than comparing claims to a simple sequence with an easy to derive limit. For an introductory example of the subtlety involved, while the two series (1/2 + 1/4 + 1/8 + ...) and (2 - 1/2 - 1/4 - 1/8 - ...) both approach 1 in opposite directions, most uncomputable numbers cannot be approached from both sides simultaneously (by a computably enumerable process, anyway). For example, while Chaitin's number is a definite number, you cannot write down any program whose sequence of outputs converges to it from above. They're all wrong. Comparing that to probably the most basic convergent infinite series in mathematics (that doesn't end in all zeros) is quite a disservice to the complexity and beauty of the field.
  - wizeman 4y ago
    > It's not possible to write an algorithm that will detect infinite loops in all programs. Actually, it is possible, if the program is not allowed to consume infinite memory. That's what these algorithms do (where "value" is the state of the finite-state machine): https://en.wikipedia.org/wiki/Cycle_detection https://en.wikipedia.org/wiki/Cycle_detection
    - deleted 4y ago
      [deleted]
wizeman 4y ago
I'm sorry, I've only gone through the first few steps of the tutorial but the initial claims have already bothered me a lot. I have to be pedantic because this is the biggest pet peeve of mine: > Turing famously showed that computers can’t decide whether your code halts. I would say this is actually false, even though almost everybody thinks it's true. At least, if you're interested in actually solving problems rather than being interested in what is mostly a mathematical/theoretical curiosity. The Halting Problem is famously only undecidable if the code you're analyzing is being modeled on a "Turing machine" or something equally "powerful" to it. The problem is, computers are not as powerful as Turing machines, and furthermore, Turing machines (or something equivalent to them) neither exist nor can ever exist in practice, because it's impossible to build a "machine" with truly infinite memory. In fact, if the machine where the code is running has finite memory, then the Halting problem is actually very easily solved (well, in theory). And there already exists various known algorithms that detect cycles of values (where the "value" in this context is the state of the program): https://en.wikipedia.org/wiki/Cycle_detection https://en.wikipedia.org/wiki/Cycle_detection As you can see, if you use one of these cycle detection algorithms, then the Halting Problem is not undecidable. It's easily solvable. The problem is that, while these known algorithms are able to solve the problem in constant memory, there are no known algorithms to solve it in a time-efficient way yet. But again, it is decidable, not undecidable. Now, I understand how Turing machines as a model can be useful, as the simplifying assumption of never having to worry about a memory limit might allow you to more easily do types of analysis that could be more difficult to do otherwise. And sure, the way the Halting Problem was "solved" was very clever (and I actually suspect that's a major reason why it has reached its current legendary status). But this simplifying assumption should have never allowed a result like the Halting Problem which is known to be wrong for the type of computing that we actually care about to be elevated to the status that it currently has, and by that I mean, to mislead everyone into thinking that the result applies to actual computers. So again, I would say, be careful whenever you see a Turing machine being mentioned. I would say it would be better to view them as mostly a mathematical/theoretical curiosity. And yes, they can also be a powerful and useful tool IF you understand its limitations. But you should never confuse this model for what actually is the real world. > Henry Rice proved a much more devastating result: “computers can’t decide anything interesting about your code’s input-output!” Since Rice's theorem (and many other computer science results!) depends on the Halting Problem being true, while it is actually false for real-world machines, my understanding is that Rice's theorem is also false for real-world machines. But Rice's theorem (and sentences like the article is using) is absolutely another example of a huge number of cases where the Halting Problem has seemingly mislead almost everyone into thinking that something can't be solved when it actually can be solved. I wonder how much more research could have advanced (like for example, in SMT solvers, formal methods, etc) if everyone actually believed that it's possible for an algorithm to decide whether your program has a bug in it. How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case? Now, I'm not a computer scientist nor a mathematician or logician. So I could be wrong. If so, I would be interested in knowing how I'm wrong, as I've never seen this issue being discussed in a thorough way. Edit: another (according to my understanding) completely misleading phrase in the tutorial exemplifying what I'm describing: > we learned Turing’s proof that halts is actually impossible to implement: any implementation you write will have a bug! Now, to be clear I'm not blaming the author of the tutorial, as this is just one very tiny example of what actually is an extremely widespread belief across the whole industry.
deleted 4y ago
[deleted]
svat 4y ago
This was very satisfying. The format works well, and makes sure you as reader are doing at least a minimum amount of thinking about the topics being presented. Even the pops and dings (if you have sound on) are fun :) This seems like a good format, and I see some other submissions from the site earlier: https://news.ycombinator.com/from?site=tigyog.app https://news.ycombinator.com/from?site=tigyog.app My only quibble with this one is with step 19 ("hangIf3") which relies on "infinity is not considered even" — that is a distraction IMO, and if I understand correctly (have not thought about this carefully) the example could be replaced with something that involves an actual odd number.
- JadeNB 4y ago
  > My only quibble with this one is with step 19 ("hangIf3") which relies on "infinity is not considered even" — that is a distraction IMO, and if I understand correctly (have not thought about this carefully) the example could be replaced with something that involves an actual odd number. Indeed, you could just replace haltIf3or7 by haltIf3or5or7 (or whatever). (And, of course, whether or not infinity is considered even cannot be deduced from the information given, so relying on this technicality here I'd argue is beyond distracting and into the realm of so underspecified that it might be wrong. Or we could raise the same objection mentioned earlier, that it's not specified what kind of object `n` is, and numeric types often have only finitely many inhabitants ….)
- jamesfisher 4y ago
  Oh hi, author here! I tend to agree on `hangIf3`. I have a habit of mixing in other kinds of puzzles. Sometimes they're fun, but sometimes they're irrelevant to the main point ... I'll rethink this one. p.s. thanks for the compliments on the format! If you (or anyone else) wants to create tutorials in this format, https://tigyog.app/ https://tigyog.app/ is a full platform for that! WYSIWYG editor and all :-)
  - psychoslave 4y ago
    Could it use more readable identifiers like `hang•if•3`? This stay valid js without mixed case found in usual code in the wild sticking to ascii. To my mind it feels like avoidable visual clutter, all the more in didactic work. Apart from that, it was nicely done all the way, congratulations and thanks for the pleasing moment.
daveguy 4y ago
The answer to at least one of these is "Yes, it solves the halting problem." This may be a semantic issue, where the author is asking if it accurately predicts halting for a single input. But that is not the definition of the "halting problem". The format is effective and interesting. But it does need some edits/clarifications.
- pseudoramble 4y ago
  Yeah this really threw me off too. I kept saying no it didn’t solve the halting problem thinking of the more generalized version, not that particular case. Eventually I got it, but not right away!
constantcrying 4y ago
I read through it, I think the idea of having regular attention checks is quite interesting. (Personally I found them to be a bit too frequent). But there are also things like: >If you implement halts using canBeRegex, you’ve got a proof by contradiction that canBeRegex can’t exist. This is plainly false. I can also implement halts using addition, that does not imply that addition can not exist. The author is clearly writing for a more general audience and I know what he means. But I think that if you are writing for a more general audience you should be more careful in your language and I think the article is sonewhat lacking there.
- Gehinnn 4y ago
  This is not false. If you can implement halt using addition, addition cannot exist. Ex falso quod libet - if you can prove a single false statement, every statement is true.
  - constantcrying 4y ago
    Here is a solution of the halting problem which is implemented using addition: function haltWithAdd(code) { var a = 1 + 2; return halt(code); } This clearly solves the halting problem (we assumed the existence of halt as the first step of our proof by contradiction). And it clearly uses addition (surely you can find where it does). By the logic (as written) of the article the implication is that '+' does not exist.
    - akdas 4y ago
      > This clearly solves the halting problem (we assumed the existence of halt as the first step of our proof by contradiction). Implementing the halting problem using addition does not assume the existence of halt. It assumes the existence of addition, and you use that to show that halt must also exist. And that's not possible to do. To implement halts using addition, you need to: - Take the input to halts, namely the source code to a program. - Convert that into an input to addition, namely two numbers. - Call into addition, which adds the numbers. - Use the result of that addition to infer whether the original program halts or not.
revskill 4y ago
Thanks ! This is inspirational. Could i know which libraries/frameworks do you use for the tutorial ? Thanks.
- schoen 4y ago
  The author said elsewhere in this thread that he uses his own invention, https://tigyog.app/ https://tigyog.app/.
alcover 4y ago
for (let i = 0; i <= i; i++); // hmm If canBeRegex is smart enough to parse `return s.length === 3;` it could also detect the for-loop has no side-effect and skip it..
- deltaseventhree 4y ago
deterministic 4y ago
The halting problem is not a big deal in practice. Plenty of compilers for many programming/proof languages out there (Agda, Idris, Coq, LEAN etc.) will reject code that the compiler can’t prove is terminating. And yet those programming languages are more than powerful enough for writing real world software. Including operating systems, compilers etc. A good introduction to this subject is the book “Type Driven Development in Idris” or one of the Agda books.
- mkleczek 4y ago
  No, dependent types are no the answer - read (or watch) this: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity
  - miloignis 4y ago
    I have in the past, and I belive that they are either mistaken or they are claiming something uncontroversial that is misunderstood. In any case, you don't need dependent types for a compiler to prove termination, it's just that most languages don't care about termination except those with dependent types. You could create a compiler for Rust that has similar termination checking to Coq, if you wanted.
    - mkleczek 4y ago
      Ahh, I misread your comment. Indeed, halting is not very interesting property of programs.
  - deterministic 4y ago
    CompCert disagrees.
moralestapia 4y ago
Hmm the format is nice but the author doesn't seem to have a good understanding of the underlying theory. For instance, question 8 describes a function that does not halt, it asks you to answer whether it halts or not (the answer is no) then it tells you it does halt (wtf) if you implement it on Javascript (wtfx2). This theory has to be approached from an abstract point of view, that kind of argument is conceptually equivalent to "it does halt because I will destroy the computer with a hammer, lol". From there it just becomes more and more deranged with each question.

184 points by lispybanana 4y ago

Detecting infinite loops (halting) isn't the impossible problem turing "proved" from my experience. Its just a lim/tends to problem. Which depends entirely on how you define infinity.

tgv 4y ago
It's not possible to write an algorithm that will detect infinite loops in all programs. But of course there are instances that can be detected, such as for () {}
- DarkmSparks 4y ago
  As I say, from my experience that depends how and if you define infinitely. If infinite is formally defined then detecting if any function equals or tends to it is fairly trivial. quick and useful defs are "can exceed a time limit", or "can exceed the error bounds of floating point math" I'd guess you can do it formally by catching the 6 or 7 definitions of infinite, but I've never come close to needing to go that far, for most, just programatically constructing a graph of the logic and detecting infinite loops in it has proved more than sufficient.
  - UncleMeat 4y ago
    Good news. Turing defined a nonterminating Turing Machine in his paper so we don't need to worry about some weird nonstandard definition of nontermination. "Oh, computers have finite memory so actually they are finite state machines" is just needless pedantry that is not useful for the actual mathematical relevance of Turing's proof and its consequences. Yes, the field of static analysis makes practical (though not flawless) solutions to undecidable problems every day. This is not relevant here.
    - insanitybit 4y ago
      damn this Turing guy sounds like he really knew what he was talking about
    - maweki 4y ago
      The great thing about undecidable problems is, that you can put an arbitrary amount of research in and you'll probably find another subclass of instances for which the problem is indeed decidable. Only an infinite number of subclasses of instances to go. That's proven job safety for computer science researchers.
      - wizeman 4y ago
        > Only an infinite number of subclasses of instances to go. There's only one subclass of instances for which the problem is undecidable: those where the program being analyzed is allowed to consume infinite memory. Which is not the same thing as saying that the program is implemented in a Turing-complete language. Because you can write a program in a Turing-complete language and yet, run it on a machine with finite memory (i.e. a computer).
    - DarkmSparks 4y ago
      nope, nothing to do with finite memory or accuracy. Thats just an easy/practical way to define it if you have a halting problem to solve. Everything to do with https://en.m.wikipedia.org/wiki/1/2_%2B_1/4_%2B_1/8_%2B_1/16_%2B_%E2%8B%AF https://en.m.wikipedia.org/wiki/1/2_%2B_1/4_%2B_1/8_%2B_1/16... halting exactly at infinity (and knowing it without summing infinitely).
      - CaptainNegative 4y ago
        If one is willing to be that vague in drawing connections, one can reduce nearly every problem to any other one. But Turing was a mathematician, and very precise with his definitions (albeit not quite as pedantic as some successors such as Aho/Ullman decades later). The interesting bit about Turing's result is that it can be adapted to a wide class of mathematical and real objects. Physical systems? Yep. Time and/or space bounded machines? You bet. Actually, at its core Turing's result is itself an adaptation of Gödel's, who more broadly talks about the context of first-order mathematical theories. If one want to bring these concepts to practice (where by practice I mean the realm of proving results in theoretical cs), it's a lot more effort than comparing claims to a simple sequence with an easy to derive limit. For an introductory example of the subtlety involved, while the two series (1/2 + 1/4 + 1/8 + ...) and (2 - 1/2 - 1/4 - 1/8 - ...) both approach 1 in opposite directions, most uncomputable numbers cannot be approached from both sides simultaneously (by a computably enumerable process, anyway). For example, while Chaitin's number is a definite number, you cannot write down any program whose sequence of outputs converges to it from above. They're all wrong. Comparing that to probably the most basic convergent infinite series in mathematics (that doesn't end in all zeros) is quite a disservice to the complexity and beauty of the field.
- wizeman 4y ago
  > It's not possible to write an algorithm that will detect infinite loops in all programs. Actually, it is possible, if the program is not allowed to consume infinite memory. That's what these algorithms do (where "value" is the state of the finite-state machine): https://en.wikipedia.org/wiki/Cycle_detection https://en.wikipedia.org/wiki/Cycle_detection
  - deleted 4y ago
    [deleted]

wizeman 4y ago

I'm sorry, I've only gone through the first few steps of the tutorial but the initial claims have already bothered me a lot. I have to be pedantic because this is the biggest pet peeve of mine: > Turing famously showed that computers can’t decide whether your code halts. I would say this is actually false, even though almost everybody thinks it's true. At least, if you're interested in actually solving problems rather than being interested in what is mostly a mathematical/theoretical curiosity. The Halting Problem is famously only undecidable if the code you're analyzing is being modeled on a "Turing machine" or something equally "powerful" to it. The problem is, computers are not as powerful as Turing machines, and furthermore, Turing machines (or something equivalent to them) neither exist nor can ever exist in practice, because it's impossible to build a "machine" with truly infinite memory. In fact, if the machine where the code is running has finite memory, then the Halting problem is actually very easily solved (well, in theory). And there already exists various known algorithms that detect cycles of values (where the "value" in this context is the state of the program): https://en.wikipedia.org/wiki/Cycle_detection https://en.wikipedia.org/wiki/Cycle_detection As you can see, if you use one of these cycle detection algorithms, then the Halting Problem is not undecidable. It's easily solvable. The problem is that, while these known algorithms are able to solve the problem in constant memory, there are no known algorithms to solve it in a time-efficient way yet. But again, it is decidable, not undecidable. Now, I understand how Turing machines as a model can be useful, as the simplifying assumption of never having to worry about a memory limit might allow you to more easily do types of analysis that could be more difficult to do otherwise. And sure, the way the Halting Problem was "solved" was very clever (and I actually suspect that's a major reason why it has reached its current legendary status). But this simplifying assumption should have never allowed a result like the Halting Problem which is known to be wrong for the type of computing that we actually care about to be elevated to the status that it currently has, and by that I mean, to mislead everyone into thinking that the result applies to actual computers. So again, I would say, be careful whenever you see a Turing machine being mentioned. I would say it would be better to view them as mostly a mathematical/theoretical curiosity. And yes, they can also be a powerful and useful tool IF you understand its limitations. But you should never confuse this model for what actually is the real world. > Henry Rice proved a much more devastating result: “computers can’t decide anything interesting about your code’s input-output!” Since Rice's theorem (and many other computer science results!) depends on the Halting Problem being true, while it is actually false for real-world machines, my understanding is that Rice's theorem is also false for real-world machines. But Rice's theorem (and sentences like the article is using) is absolutely another example of a huge number of cases where the Halting Problem has seemingly mislead almost everyone into thinking that something can't be solved when it actually can be solved. I wonder how much more research could have advanced (like for example, in SMT solvers, formal methods, etc) if everyone actually believed that it's possible for an algorithm to decide whether your program has a bug in it. How many good people were discouraged into going into this area of research because of this widespread belief that this pursuit is proven to be unachievable in the general case? Now, I'm not a computer scientist nor a mathematician or logician. So I could be wrong. If so, I would be interested in knowing how I'm wrong, as I've never seen this issue being discussed in a thorough way. Edit: another (according to my understanding) completely misleading phrase in the tutorial exemplifying what I'm describing: > we learned Turing’s proof that halts is actually impossible to implement: any implementation you write will have a bug! Now, to be clear I'm not blaming the author of the tutorial, as this is just one very tiny example of what actually is an extremely widespread belief across the whole industry.

deleted 4y ago

[deleted]

svat 4y ago

This was very satisfying. The format works well, and makes sure you as reader are doing at least a minimum amount of thinking about the topics being presented. Even the pops and dings (if you have sound on) are fun :) This seems like a good format, and I see some other submissions from the site earlier: https://news.ycombinator.com/from?site=tigyog.app https://news.ycombinator.com/from?site=tigyog.app My only quibble with this one is with step 19 ("hangIf3") which relies on "infinity is not considered even" — that is a distraction IMO, and if I understand correctly (have not thought about this carefully) the example could be replaced with something that involves an actual odd number.

JadeNB 4y ago
> My only quibble with this one is with step 19 ("hangIf3") which relies on "infinity is not considered even" — that is a distraction IMO, and if I understand correctly (have not thought about this carefully) the example could be replaced with something that involves an actual odd number. Indeed, you could just replace haltIf3or7 by haltIf3or5or7 (or whatever). (And, of course, whether or not infinity is considered even cannot be deduced from the information given, so relying on this technicality here I'd argue is beyond distracting and into the realm of so underspecified that it might be wrong. Or we could raise the same objection mentioned earlier, that it's not specified what kind of object `n` is, and numeric types often have only finitely many inhabitants ….)
jamesfisher 4y ago
Oh hi, author here! I tend to agree on `hangIf3`. I have a habit of mixing in other kinds of puzzles. Sometimes they're fun, but sometimes they're irrelevant to the main point ... I'll rethink this one. p.s. thanks for the compliments on the format! If you (or anyone else) wants to create tutorials in this format, https://tigyog.app/ https://tigyog.app/ is a full platform for that! WYSIWYG editor and all :-)
- psychoslave 4y ago
  Could it use more readable identifiers like `hang•if•3`? This stay valid js without mixed case found in usual code in the wild sticking to ascii. To my mind it feels like avoidable visual clutter, all the more in didactic work. Apart from that, it was nicely done all the way, congratulations and thanks for the pleasing moment.

daveguy 4y ago

The answer to at least one of these is "Yes, it solves the halting problem." This may be a semantic issue, where the author is asking if it accurately predicts halting for a single input. But that is not the definition of the "halting problem". The format is effective and interesting. But it does need some edits/clarifications.

pseudoramble 4y ago
Yeah this really threw me off too. I kept saying no it didn’t solve the halting problem thinking of the more generalized version, not that particular case. Eventually I got it, but not right away!

constantcrying 4y ago

I read through it, I think the idea of having regular attention checks is quite interesting. (Personally I found them to be a bit too frequent). But there are also things like: >If you implement halts using canBeRegex, you’ve got a proof by contradiction that canBeRegex can’t exist. This is plainly false. I can also implement halts using addition, that does not imply that addition can not exist. The author is clearly writing for a more general audience and I know what he means. But I think that if you are writing for a more general audience you should be more careful in your language and I think the article is sonewhat lacking there.

Gehinnn 4y ago
This is not false. If you can implement halt using addition, addition cannot exist. Ex falso quod libet - if you can prove a single false statement, every statement is true.
- constantcrying 4y ago
  Here is a solution of the halting problem which is implemented using addition: function haltWithAdd(code) { var a = 1 + 2; return halt(code); } This clearly solves the halting problem (we assumed the existence of halt as the first step of our proof by contradiction). And it clearly uses addition (surely you can find where it does). By the logic (as written) of the article the implication is that '+' does not exist.
  - akdas 4y ago
    > This clearly solves the halting problem (we assumed the existence of halt as the first step of our proof by contradiction). Implementing the halting problem using addition does not assume the existence of halt. It assumes the existence of addition, and you use that to show that halt must also exist. And that's not possible to do. To implement halts using addition, you need to: - Take the input to halts, namely the source code to a program. - Convert that into an input to addition, namely two numbers. - Call into addition, which adds the numbers. - Use the result of that addition to infer whether the original program halts or not.

revskill 4y ago

Thanks ! This is inspirational. Could i know which libraries/frameworks do you use for the tutorial ? Thanks.

schoen 4y ago
The author said elsewhere in this thread that he uses his own invention, https://tigyog.app/ https://tigyog.app/.

alcover 4y ago

for (let i = 0; i <= i; i++); // hmm If canBeRegex is smart enough to parse `return s.length === 3;` it could also detect the for-loop has no side-effect and skip it..

deltaseventhree 4y ago

deterministic 4y ago

The halting problem is not a big deal in practice. Plenty of compilers for many programming/proof languages out there (Agda, Idris, Coq, LEAN etc.) will reject code that the compiler can’t prove is terminating. And yet those programming languages are more than powerful enough for writing real world software. Including operating systems, compilers etc. A good introduction to this subject is the book “Type Driven Development in Idris” or one of the Agda books.

mkleczek 4y ago
No, dependent types are no the answer - read (or watch) this: https://pron.github.io/posts/correctness-and-complexity https://pron.github.io/posts/correctness-and-complexity
- miloignis 4y ago
  I have in the past, and I belive that they are either mistaken or they are claiming something uncontroversial that is misunderstood. In any case, you don't need dependent types for a compiler to prove termination, it's just that most languages don't care about termination except those with dependent types. You could create a compiler for Rust that has similar termination checking to Coq, if you wanted.
  - mkleczek 4y ago
    Ahh, I misread your comment. Indeed, halting is not very interesting property of programs.
- deterministic 4y ago
  CompCert disagrees.

moralestapia 4y ago

Hmm the format is nice but the author doesn't seem to have a good understanding of the underlying theory. For instance, question 8 describes a function that does not halt, it asks you to answer whether it halts or not (the answer is no) then it tells you it does halt (wtf) if you implement it on Javascript (wtfx2). This theory has to be approached from an abstract point of view, that kind of argument is conceptually equivalent to "it does halt because I will destroy the computer with a hammer, lol". From there it just becomes more and more deranged with each question.