4 ms·

> We're interested in the common case, which requires years of empirical observation. You, perhaps. I'm interested in how much things can be simplified. It's a

> We're interested in the common case, which requires years of empirical observation. You, perhaps. I'm interested in how much things can be simplified. It's a different kind of experiment: “If we prioritize simplicity and correctness, and say to hell with every other consideration, what kinds of programs can we write?” > Deductive proofs (with Isabelle, PVS, Coq etc.) is used only to tie together results of automated methods, or fill in the holes where automated methods have failed. I count fancy proof assistants among those technologies I don't want to have to trust anymore. When I read a proof script full of complicated tactics, my eyes glazeth over. > I don't think anyone believes that "ordinary" non-high-assurance real software (aside from certain very small core components) would be verified by deductive proof any time in the next few decades. If “real world software” presupposes this attitude of not wanting to do things the right way, I'm not terribly interested in it. > But software requirements aren't for 100% confidence in correctness, if only because you don't get anywhere near that with the hardware the software is running on. Hardware failure is Not My Problem (tm). I just want it not to be my fault when things go wrong. > What the formal methods community is really interested in these days is how to reduce the cost of verification required to achieve current (and near-future) correctness requirements. As I told other people, I'm not interested in “communities”.

pron 10y ago
> It's a different kind of experiment: “If we prioritize simplicity and correctness, and say to hell with every other consideration, what kinds of programs can we write?” I understand, but you must realize that we're not starting from scratch here, and we do know some things. The people who wrote, say, CompCert and seL4 did so with the exact same goals. It took them 20 man years for a small, pretty simple program, and they believe they can do it in 5. > When I read a proof script full of complicated tactics, my eyes glazeth over. Well, you should take a look at TLAPS[1], the TLA+ proof system. It's a structured, declarative proof language (Isabelle also has a declarative proof language called Isar), whose proofs look like those in the appendix of this paper[2], and are made to be readable to humans. I should say that informal proofs of algorithms have not once and not twice been found (by automated tools like model checkers or by using structured proofs) to be wrong.. > If “real world software” presupposes this attitude of not wanting to do things the right way, I'm not terribly interested in it. The "right way" isn't a decree from God. What's right for real-world software is dictated by its requirements, which include functional requirements, performance requirements, maintenance requirements, security requirements etc.. A software that's build the "right way" is one that meets its requirements while spending as little as possible to do so. A recpie app that has zero bugs of any kind and takes 7 years to build is not built the "right way", just as one-use plastic cups built with carbon fibers and costing $10 a piece is not built the right way. A recipe app shouldn't lose your recipes, but other than that, wanting to ensure no GUI bugs of any kind shouldn't drive up its cost much. > I just want it not to be my fault when things go wrong. Yes, but your customers wouldn't want to pay you 10x or 50x as other developers just to make sure your software doesn't have bugs of the type they don't really care about, nor do they want or need 0 chance of critical failure from your software. You can make make the chance of a critical problem being your fault extremely low without waterproof end-to-end verification. How much more will you be willing to invest to drive those chances from 10^-7 to 10^-8? > As I told other people, I'm not interested in “communities”. Well, you can be interested in building a spaceship that can go faster than light by warping space and not be willing to compromise on anything less, but if there's no one in the research community but you working on that problem, your chances of actually flying in such a spaceship are slim. I think that at the very least you should want to know about past and current research and its findings, if only to save you a lot of repeated work. [1]: https://tla.msr-inria.inria.fr/tlaps/content/Home.html https://tla.msr-inria.inria.fr/tlaps/content/Home.html [2]: http://lamport.azurewebsites.net/pubs/proof.pdf http://lamport.azurewebsites.net/pubs/proof.pdf

pron 10y ago

> It's a different kind of experiment: “If we prioritize simplicity and correctness, and say to hell with every other consideration, what kinds of programs can we write?” I understand, but you must realize that we're not starting from scratch here, and we do know some things. The people who wrote, say, CompCert and seL4 did so with the exact same goals. It took them 20 man years for a small, pretty simple program, and they believe they can do it in 5. > When I read a proof script full of complicated tactics, my eyes glazeth over. Well, you should take a look at TLAPS[1], the TLA+ proof system. It's a structured, declarative proof language (Isabelle also has a declarative proof language called Isar), whose proofs look like those in the appendix of this paper[2], and are made to be readable to humans. I should say that informal proofs of algorithms have not once and not twice been found (by automated tools like model checkers or by using structured proofs) to be wrong.. > If “real world software” presupposes this attitude of not wanting to do things the right way, I'm not terribly interested in it. The "right way" isn't a decree from God. What's right for real-world software is dictated by its requirements, which include functional requirements, performance requirements, maintenance requirements, security requirements etc.. A software that's build the "right way" is one that meets its requirements while spending as little as possible to do so. A recpie app that has zero bugs of any kind and takes 7 years to build is not built the "right way", just as one-use plastic cups built with carbon fibers and costing $10 a piece is not built the right way. A recipe app shouldn't lose your recipes, but other than that, wanting to ensure no GUI bugs of any kind shouldn't drive up its cost much. > I just want it not to be my fault when things go wrong. Yes, but your customers wouldn't want to pay you 10x or 50x as other developers just to make sure your software doesn't have bugs of the type they don't really care about, nor do they want or need 0 chance of critical failure from your software. You can make make the chance of a critical problem being your fault extremely low without waterproof end-to-end verification. How much more will you be willing to invest to drive those chances from 10^-7 to 10^-8? > As I told other people, I'm not interested in “communities”. Well, you can be interested in building a spaceship that can go faster than light by warping space and not be willing to compromise on anything less, but if there's no one in the research community but you working on that problem, your chances of actually flying in such a spaceship are slim. I think that at the very least you should want to know about past and current research and its findings, if only to save you a lot of repeated work. [1]: https://tla.msr-inria.inria.fr/tlaps/content/Home.html https://tla.msr-inria.inria.fr/tlaps/content/Home.html [2]: http://lamport.azurewebsites.net/pubs/proof.pdf http://lamport.azurewebsites.net/pubs/proof.pdf