> Additionally, you can have a language like Rust that lets the programmer poke holes in the type system, which is useful in practice but makes the type system

> Additionally, you can have a language like Rust that lets the programmer poke holes in the type system, which is useful in practice but makes the type system no longer guarantee what it says it guarantees. FWIW, Rust has a pile of behaviours that are undefined behaviour[1]: that is, the compiler will optimise/reason assuming they never happen. These are impossible to hit in safe code, but are possible with `unsafe`, it's up to the programmer to manually maintain them. That is, the type system does guarantee certain things, and it's up to the programmer to not break it inside `unsafe`. [1]: http://doc.rust-lang.org/master/rust.html#behavior-considered-unsafe http://doc.rust-lang.org/master/rust.html#behavior-considere...