rm -rf /

External Content not shown. Further Information.

I am not a professional software developer — well, I guess in some sense I am, but at least not an industrial professional software developer. But at least what I heard from some industrial software developers, what I will describe now is a usual experience:

You develop a complex piece of software. Especially the "practical" pieces of software are usually evolutionally grown and very complex. And usually, when writing code, you write something very specific and nontrivial – because if it was trivial, there would usually be no reason to write it, except exercising, which is also pointless if the solution is trivial to you.

So what happens to me often (and as far as I heard, I am not alone with this) is that I wrote a large piece of software, and then compile and test it – just to eliminate the worst bugs and lots of small mistakes. I really hate this phase of writing code.

So recently, I had to optimize a functional algorithm. I did so, and it was really hard, it took me a few hours. Then I leaned back and had this feeling that I always have before the first debugging phase.

But just a few moments later I remembered: The code I have written was functional for a reason: The entire algorithm was formally verified against a specification which I already had debugged and reviewed thoroughly. Admittedly it took me longer to write verified code than it would have taken to write unverified code, but the whole phase of testing and debugging is practically nonexistent.