> I don't think human programmers have any hope of ever being able to maintain noncompositional program properties for nontrivial programs We do it all the tim

> I don't think human programmers have any hope of ever being able to maintain noncompositional program properties for nontrivial programs We do it all the time. Whatever it is that you want your program to do, and any interesting functional property of it, is a non-compositional property. I know that because if it were compositional, you wouldn't need to write the program. A property P is compositional with respect to terms A and B and composition ∘, if P(A) and P(B) implies P(A∘B) (or more strongly, iff). Compositional and inductive are the same thing if A and B can be any language term. For example, type preservation is a compositional property for, say, ML, and memory safety is a compositional property for, say, Java. > a human working on the codebase will still need a deductive-proof-like understanding. I think this is not true, either in principle or in practice: https://pron.github.io/posts/people-dont-write-programs https://pron.github.io/posts/people-dont-write-programs I know I certainly don't have anything close to a deductive understanding of the program I'm working on, but I do have such understanding of the specific pieces of code I'm writing. This is insufficient for a useful formalization of a program, because correctness properties aren't compositional, meaning that, in general, a sound specification of a program component would either be insufficient or unhelpful (i.e. no easier than the code itselg) for the writing of other components. Sure, in some cases it can be, but those are usually the easy cases. We need help with the hard ones. I totally agree that we try to isolate components and expose them with APIs, but 1. the specification here is imprecise and "soft", and 2. as the results in my "correctness and complexity" show, this does not necessarily make deduction easier (https://news.ycombinator.com/item?id=20714920 https://news.ycombinator.com/item?id=20714920). But what you should be asking is this: as there haven't been any major relevant breakthroughs in formal logic in the past couple of decades, nor in any relevant proof techniques (we still use deduction for safety properties), our deductive proof capabilities aren't significantly higher now than they were 30 years ago. If it's all a matter of discipline, then, how come we're still not able to affordably (or at all, if the programs are not tiny) verify programs with deductive proofs? > how's that any different from what I'd do using any other technique? I'm not sure I understand the question, but the last thing you want is a rich specification language that forces you to use a particular verification technique, and that's exactly what dependent types do. You want to specify whatever helps you, and then you want to verify using whatever technique you need or can afford, to reach the appropriate level of cost/benefit for your requirements. > But isn't it much the same process with a detached proof of the program property? To be honest, I don't know that dependent types are harder than "detached" deductive proofs, but this is something that Neel Krishnaswami (who's an advocate of dependent type advocate) mentioned to me as his observation (he's also the one who told me about attempts to build "gradual" dependent types to alleviate some of the other downsides I mentioned.) This can also be an upside, because it may making writing some proofs easier, as you write the program with them in mind. Either way, I think deductive proofs are, at the moment, too far behind other verification techniques to contrast different kinds of deductive proofs. But this certainly strikes me as an engineering problem.