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

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.