I know we are talking about the Platonic ideal of a perfectly sound and logical type system where absolutely nothing ever goes wrong, or at least comparing existing systems to that seemingly impossible ideal but... In the real world, if "proving False" summons dragons, then... just don't do that? I don't think there will ever be a programming language where nothing can go wrong. Safe-er languages are good, but they are not an excuse to absolve oneself of the responsibility to check one's assumptions and react to problems that happen anyway. It sounds dumb to say "just don't make errors" but even dumber to assume "errors cannot be made", so we always have to program defensively, even in "safe" languages.