[Dewie]

> 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.

[ggchappell]

> Is the distinction or separation necessarily obvious?

I don't think so, but in practice it usually is obvious, in the programming languages that actually get used.

OTOH, the notion that the compile-time language and the run-time language could be very similar is an idea that might be slowly catching on. We'll see ....