Crashing is termination; the reason it's tricky is that we often treat programs as having return type "Foo" when they actually have return type more like "Foo |

Crashing is termination; the reason it's tricky is that we often treat programs as having return type "Foo" when they actually have return type more like "Foo | Stacktrace". (Sometimes it's easier to do theoretical work by replacing crashes with infinite loops; but that's only because it's impossible to do the converse ;) )