> On the other hand, in a statically typed language there is necessarily a distinction between code that is executed at runtime and (although we often don't talk about it this way) code that is executed at compile time.

Is the distinction or separation necessarily obvious? Statically typed languages which have a unified term- and type-level seem to get a bit subtle in this regard, since a type can be used as a value. And Idris passes proofs around, and has to use proof erasure in order to not let it infect the runtime: proofs can remain until run-time if you're not careful.

I am asking this as a question since I don't have enough experience with such languages to really know myself.