3 ms·
Most strongly typed languages have such escape hatches ("Unsafe" in haskell, "Obj" in OCaml, "trustme" in Idris,....) . It's something you always need at some p
by Drup 8y ago
Most strongly typed languages have such escape hatches ("Unsafe" in haskell, "Obj" in OCaml, "trustme" in Idris,....) . It's something you always need at some point when the typing is not sufficient to properly account for what you are doing.
For instance, Coq code can be extracted to OCaml code. OCaml type system is less powerful than Coq's, so Coq needs to cheat, and the emitted code is full of "unsafe" features. But the program was typechecked with Coq's type system, and is thus perfectly safe.
Of course, the goal of the language designer is to minimize its usage. That's something the Rust people understood very well, and the unsafe blocks are an extremely good solution to this problem.
- 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?