There's even work to address that with linking types: https://dbp.io/pubs/2017/linking-types-snapl.pdf https://dbp.io/pubs/2017/linking-types-snapl.pdf If the

There's even work to address that with linking types: https://dbp.io/pubs/2017/linking-types-snapl.pdf https://dbp.io/pubs/2017/linking-types-snapl.pdf If the component is externally type-checked, the integration can be type checked against the language including it. They're also working on verifying compilers that do that: https://dbp.io/essays/2018-04-19-how-to-prove-a-compiler-fully-abstract.html https://dbp.io/essays/2018-04-19-how-to-prove-a-compiler-ful... Previously, others made the assembly languages themselves type-safe. Example: https://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf https://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf We might eventually be able to drop a caveat or three when talking about where type/memory safety ends. Cool stuff, eh?