I think his take on “debug-ability > correct by construction,” has to assume that you can understand the problem or can understand the problem. In my experience

I think his take on “debug-ability > correct by construction,” has to assume that you can understand the problem or can understand the problem. In my experience this works fine when you have a mostly procedural process on a single machine. Set some watchers, step through execution, pause to inspect state. It is much harder to do with concurrency. And damn near impossible with distributed systems. As someone who has claimed to use these kinds of tools to verify protocols, I’m curious what cases he would break this preference for debugging over reasoning. Or is the contradiction intentional? I was big into Common Lisp for years and mostly into Haskell and Lean now. I still think debugging is fine and useful to do but I get the most bang out of being able to reason about my program before I run it. Once you have the definitions and proofs in place running the code is fine I guess but all the work is done. Whereas with more dynamic systems the work has barely begun: now I need to bump into all of the errors in my code while it is running. There are times when I want both and I don’t think the computing world needs to pick one and only one.