Yes, all computation done at runtime can be done at compile time (within type system). This is a problem in some cases e.g. if you write an infinite loop, this

Yes, all computation done at runtime can be done at compile time (within type system). This is a problem in some cases e.g. if you write an infinite loop, this would mean compilation will infinitely loop. Different languages deal with this problem differently. E.g. in Agda, there is a "safe" subset of language that is not Turing Complete such that all programs can be algorithmically proven to be halting. But you can work around this via pragmas. Speaking from experience, the safe subset of Agda is all you need to write useful programs. You just need a tiny shell (maybe only few lines of code) that will handle IO and Haskell FFI. The rest of the code will be purely functional, safe, Turing Incomplete Agda.