> All practical languages (even Rust and Haskell) fail for "division by zero"
Well, they don't have dependent types. In something like Idris you can do safe natural division.
> most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks.
The difference is that those escape hatches are explicit, and used rarely enough that you can give them special attention in testing/code review - in those languages it's not 95% typechecked but more like 99.9%. (Indeed in Haskell you can use a flag to disallow bypassing the typesystem entirely, and people do).
Well, they don't have dependent types. In something like Idris you can do safe natural division.
> most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks.
The difference is that those escape hatches are explicit, and used rarely enough that you can give them special attention in testing/code review - in those languages it's not 95% typechecked but more like 99.9%. (Indeed in Haskell you can use a flag to disallow bypassing the typesystem entirely, and people do).