Yes. This is something I've been thinking about a lot, as it happens! In particular, one of the great benefits of pure languages from an optimisation standpoint

Yes. This is something I've been thinking about a lot, as it happens! In particular, one of the great benefits of pure languages from an optimisation standpoint is that unused values can always be optimised away, but this is not the case if we treat termination (or non-termination) as a side effect! For now, I'm treating it as not being a side-effect (as does C++, although C++ goes a step further and treats it as straight-up UB in certain conditions). This is something I've still yet to nail down semantically.