The importance of proofs

For at least 2 thousand years mathematicians have been constructing proofs, and everyone else has been saying "that is not important to me, I'm only interested in algorithms for real world problems". Now two things are happening: proofs are important; computer software can help us check them and even generate them.

Bug hunting can be a fun intellectual exercise. Here's a nice story if you like that sort of thing: http://arstechnica.com/information-technology/2015/05/the-discovery-of-apache-zookeepers-poison-packet/. What it illustrates is the ubiquity of software bugs. We already knew that because of all the security bugs that hackers (good and bad) love to find.

What we want is that software is proved to be correct to the greatest extent possible. One thing we explicitly don't want is perfection, which is unattainable. The weakness of perfect systems is one of the key discoveries of 20th century mathematics. What we want is to know the axioms that we are assuming, and the things that we expect to be true which we don't yet have a proof for.

So what do we do about assumptions that we don't have a proof for? Use Science. Experiment. In other words: test. Try to disprove it. Testing is expensive and error-prone. The reason for proving as much as possible is exactly so that we know what needs to be tested and to reduce that to as little as possible.

So who is going to build these software development systems incorporating proof technology? We can't trust government research to do it, because governments everywhere are addicted to using software bugs as a vector for surveillance and even for acts of war. It will need to be done by the independent open source community. Doing this will be the 21st century equivalent of defending freedom by bearing arms in a well regulated militia.