[jeberle]

Does Rice's theorem cover this?

> [ all non-trivial semantic properties of programs are undecidable ]

https://en.wikipedia.org/wiki/Rice's_theorem

Found here:

From Sumatra to Panama, from Babylon to Valhalla

https://www.youtube.com/watch?v=bE1bRbZzQ_k&t=48m27s

[penteract]

No. Being well typed is not a semantic property of of a program - in a language where it makes sense to talk about running badly typed code, a piece of code that starts with an infinite loop may be well or badly typed after that point with no observable difference in program behaviour.

There are decidable type systems for Turing complete languages (many try to have this property), and there are languages in which all well typed programs terminate for which type checking is undecidable (System F without all type annotations).