2 ms·
> It's something you always need at some point when the typing is not sufficient to properly account for what you are doing. E.g. FFI becomes horrendously impr
by pdpi 8y ago
> It's something you always need at some point when the typing is not sufficient to properly account for what you are doing.
E.g. FFI becomes horrendously impractical without something of this kind.
- nickpsecurity 8y agoThere'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?