On Thursday, 17 October 2019 at 18:53:29 UTC, Paul Backus wrote: > https://blog.sigplan.org/2019/10/17/what-type-soundness-theorem-do-you-really-want-to-prove/ I will give that a read, thanks.