> Humans are pretty good at doing proofs A few problems with human-style proofs: * Cost of proof construction: Using computational tools allows us to offload

> Humans are pretty good at doing proofs A few problems with human-style proofs: * Cost of proof construction: Using computational tools allows us to offload large portions of the proof to decision procedures, automated proof strategies, and invariant generators. This substantially reduces the effort involved in coming up with a proof in the first place. * Cost of validation: Humans make mistakes all the time. Peer/self reviewing a proof of that size and complexity in order to ensure that the proof does not contain errors will dominate the total proof writing time. (Edit: with computers we get proof checking for free.) > Now obviously the state of the art is progressing and it's getting easier to formally verify properties of programs, but I wonder whether it will ever be feasible to make this part of everyday software development. Part of the reason for doing these large verification projects is to figure out what, exactly, makes verification so difficult and time-consuming. And then developing new technology to make formal proof development cheaper. Many of these large verification efforts result in an offshoot of papers about new techniques for proving, or new design considerations for theorem provers, or new libraries that will make similar proofs in the future easier.