Not necessarily. You should be able to write a halting computation to determine whether a number is prime in a Turing complete language. It may be stupid hard to encode, or take a really long time to run, however.

The halting problem says that you can't write a halting decision procedure that takes an arbitrary program as input and determines whether that program halts, for any program. That doesn't mean that no programs halt. On the contrary, most programs in Turing complete languages obviously do halt and it's often trivial to tell if a particular program halts or not (e.g., `print "hello"` obviously halts). A Turing complete language can compute anything that is computable. So if the type system is Turing complete, you should be able to type a function that only takes primes... in theory.

I don't understand how this is fundamentally different from just doing it in regular javascript. You could write a javascript function that recurses forever on condition x: just write a function that calls itself with the same parameters unless condition x is met. How is it fundamentally different if the type system does it?

> How is it fundamentally different if the type system does it?

runtime vs compile time. For example someone could write some TypeScript that would forever compile, which is intuitively unexpected when compiling.