> Being 95% typechecked (or 95% statically checked) turns out to be a lot like being 0% typechecked.
That's just not realistic. All practical languages (even Rust and Haskell) fail for "division by zero", and most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. Still (some) people see a lot of value in _more_ static (type/contract) checking.
> 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).
That's just not realistic. All practical languages (even Rust and Haskell) fail for "division by zero", and most (all?) (again even Rust and Haskell) offer escape hatches for their otherwise rather strong static checks. Still (some) people see a lot of value in _more_ static (type/contract) checking.