Hacker News new | ask | show | jobs
by s_ngularity 2992 days ago
The author's use of "type soundness" matches the precise, widely-accepted mathematical definition which is used in the literature. Type soundness does not require total functions, although they certainly make it simpler.

It is possible to encode the semantics of exceptions such that a reasonable definition of soundness is still provable. See, for instance, Chapter 14 of Types and Programming Languages by Pierce.