Hacker News Reader

But you can do some static analysis on it. There is most likely a very common set of patterns known to terminate, a rare-but-expected set of patterns known to never terminate, and an infinite set of rare patterns which is unknown.

Rust is doing basically the same thing. Default code is "safe", and the compiler is able to prove its correctness. If the compiler can't make heads or tails of it, you have to put it in "unsafe" - and the programmer is expected to check the correctness herself.

That is true in general, yes.

This is also true of Python, but a program which is just `print("hi!")` can be statically proven to halt.

I suspect this is true of a very great majority of type hints in Python which actually exist.

But you can know if it has halted. And if you're a linter, you know how long it took to halt last time. So you can keep track of the times and if it goes from 200ms to 210ms to to 215ms to 10s-and-counting you can let the user know that something significant has changed without being sure that it won't halt any second now.