5 ms·

Eventually, we need to move towards formally verified software. Some bugs slip past any number of human eyeballs. It won't be feasible to do formal verification

• mcdoug 12y ago
  I feel like if we did this we'd never get to an actual working system. How do you formally verify that a remote file system interacting with a faulty hard disk is doing the right thing? This reminds me of Hurd, which is arguably a superior design that will never be finished.
  • fdej 12y ago
    That's certainly an issue, and there's no easy way around the fact that even formally specifying the behavior of a program that has to interact with the outside world is problematic. Nonetheless, some of the academic research that has been done on formal verification is quite impressive (including the development of actual nontrivial working software). And it can be done piecemeal -- you could formally certify the functional parts of a crypto library (and demand this standard of future replacements) independently of what goes on in the world of file system drivers. Realistically speaking, as worse is better, I think a large push for formally verified software probably won't happen for decades to come, but it will happen eventually. It already happened in parts of the hardware industry (Intel certainly don't want the division bug to happen ever again). The main issue is that we need tools that make development easier, to allow keeping up with the rapidly changing requirements in the software world.
    • jdc 12y ago
      What are some examples of non-trivial working formally verified software?
      • fdej 12y ago
        http://compcert.inria.fr/ http://compcert.inria.fr/ is the first that comes to mind.
      • maemre 12y ago
        There is Quark [1], a web browser with formally verified kernel. Here, kernel is a process which manages other slave (helper) processes which render the page actually. [1]: http://goto.ucsd.edu/quark/ http://goto.ucsd.edu/quark/
    • lgunsch 12y ago
      >we need tools that make development easier, to allow keeping up with the rapidly changing requirements in the software world. The practice of Test driven development is a great solution to this. The problem is very few people use it, many people actually are against it, and many of those that do do it, do it incorrectly (not on purpose). I would think that small chunks of singly-purposed functionality would be much easier to verify.
      • schoen 12y ago
        There's kind of a considerable gap between formally verified software and test-driven development, though. For example, a parser or the routines that go into it might pass dozens or hundreds of unit tests, yet still fail to parse certain inputs correctly, fail to parse them in exactly the same way as another parser (as Langsec researchers have emphasized, often producing possible time-of-check/time-of-use vulnerabilities), or even have a memory corruption bug. I don't mention this in order to criticize test-driven development or the improvements it can bring to software reliability or safety, just to point out that there's still a big gap from there to a formal proof of correctness.
• cheatsheet 12y ago
  Sure, but there will still be bugs. We might have to figure out what a bug is semantically on the next layer of abstraction as we are developing it (and have the capacity to formally describe it), but there will be opinions, and thus there will be bugs.
  • fdej 12y ago
    Of course. In the end, we don't even have a perfect understanding of the physics on which digital technology is built. Nonetheless, we can evidently do much better than we do today, and delegate more of the hard work to our robotic slaves.
    • cheatsheet 12y ago
      I think a wise person would hesitate at judging a task hard or easy.