Whenever I reach the point where static analysis can't help me any further I always feel a sort of thrill mixed with terror. This is the real deal. Until now the problems were easy to find, the questions had well defined answers to choose from, the rules were universal. In the part of the logic that cannot be checked, the invariants upheld manually, where the best the type system can enforce is for the programmer to clearly state what they're doing, lies the real beast. In proofs commented on functions or invariants as logical expressions over plain English variables written in the doc comments of a struct.

In the blurry and pompous future I imagine for software development, that's where the programmer's time will be spent. Once we all agree on what a string is, what it means to depend on someone else's code, and what parts a UI should be made of, all a developer should have to do is make decisions and derive proofs an automated deduction engine can't do on its own.