This is all pretty fun reading. At least with my own code in Haskell, I work in the mental model where I assume termination and strong normalization (all progr

This is all pretty fun reading. At least with my own code in Haskell, I work in the mental model where I assume termination and strong normalization (all programs terminate under all evaluation strategies). Then, Bottom corresponds to either an exception that will get forced or a computationally boring infinite loop (which the rts can sometime detect and turn into an exception). My personal style favors having those errors be very very visible. That said, depending on what formal or informal reasoning properties you care about (especially as a library writer), these little subtleties can be really important!