3 ms·

Would you actually do this, or do you just like to imagine a world where people do this? I'm familiar with Coq and Prolog(one of which I think you're hinting a

• agentultra 11y ago
  I learning to use these techniques in my everyday work (cloud software). I think of it like this: nobody is going to care if I screw up the script to balance my accounts. If I write some software that messes up the balance of everyone's account in some bank then someone is going to care. I don't think formal methods and rigor are the sole domain of government institutions, avionics control software, and industrial robotics. The public relies on the cloud and the applications that run on it and they have no recourse if their data is exposed or disappears. Imagine if instead of crossing over a bridge you were stopped at a booth and asked to sign a wager stating that nobody is liable if the bridge collapses underneath you while you cross it. Rich or poor, regardless of how much you pay in taxes, you should be able to rely on that bridge being built to the highest standards we know how and someone should be liable if it falls down. You can rely on this in real life. Why do we not have this for software? I'm not saying I write all of my software using formal methods and rigorous proofs. It's often good enough to sketch my idea on the back of a napkin when I'm building a tool shed. But nobody built a sky-scraper without doing a little math and being fairly rigorous in their thinking.