The visible "productivity" as in manager friendly LOC. The actual productivity goes up.
Managers don't want that though, for reasons that already Dijkstra has outlined.
Managers don't want that though, for reasons that already Dijkstra has outlined.
Proofs are hard and often not for interesting reasons; its stuff like proving that you won't overflow a 2^64 counter which you only increment (aka something which won't happen for another couple billion years).
Current tools are only useful for specific kinds of problems in specific domains; things where a life really depends on correctness. Outside of those cases, lightweight techniques provide much more bang for your buck imo.