> Now wait a minute, I’m sure you’re thinking. I’ve never proved sh*t about my functions. I’m betting that you have. And that you do all the time. You’re always

> Now wait a minute, I’m sure you’re thinking. I’ve never proved sh*t about my functions. I’m betting that you have. And that you do all the time. You’re always convincing yourself that your function is doing the right thing. Yours may not be a formal proof (which may be what leads to some bugs), but reasoning about code is something that software developers do all the time. They’re playing the code back in their head to see how it behaves. I sometimes try to point this out when arguing in favor of Formal Methods. You're already using informal Formal Methods anyway. Just write your reasoning down and make the computer double-check it. "Oh the expense!" I hear them cry. But where's the spreadsheet comparing that with the expense of the faulty reasoning? Where is the Manhattan Project to lower the cost of logic? And don't get me started on (what Guy Steele Jr. calls) Computer Science Meta-notation, which has no official standard, and isn't a runnable language. ( https://groups.csail.mit.edu/mac/users/gjs/6.945/readings/Steele-MIT-April-2017.pdf https://groups.csail.mit.edu/mac/users/gjs/6.945/readings/St... )