I want to qualify your (1) a bit—there's actually enormous value in "partially proved" systems in a sense. At the very least, that 30% is something you won't ha

I want to qualify your (1) a bit—there's actually enormous value in "partially proved" systems in a sense. At the very least, that 30% is something you won't have to think about every again so long as the spec it's met works for what you need. But what I really wanted to talk about is the exciting stuff going on in languages like Idris where programming is paramount and proving is just there for support. In a situation like this, your goal is less to arrive at 100% formally proven systems, but instead steal 90% of the power of a proof assistant to build more maintainable, powerful code. In this case, you're quite likely to only prove 30% of your code, the skeleton perhaps, and leave the rest. The result is often however that when you do this, the remaining 70% of the code is so restricted by your design that there are only a handful of ways to continue and they're likely all the right behavior. A great example of this is Ur/Web which uses just a little bit of dependent typing to ensure that the names in your forms, domain, and databases all match up. It means you design your entire system around those names (your domain) and prove it to be formally consistent. Then the remaining design space is tiny and it's easy to write a good program. ... Or even to augment that skeleton with a security policy and have static flow control analysis "for free". (That said, Ur/Web is a prototype system with minimal documentation, so I won't recommend it as an actual "system of the future"... just a glimpse.)