Why do earthlings do buggy software and hardware

I think no one will argue with the fact that the quality of the complex systems created by earthlings is far from ideal. Of course, it can be said that everything works — airplanes are flying, spacecraft plowing the orbits of the Earth, etc.

But at the same time, everybody got used to the fact that the software on their devices works unpredictably, one time, that even installing the latest updates does not guarantee the absence of security problems, which often in open, massively used code find errors that exist there for many years, which even Large and "technological" companies are failures and data leaks, that spacecraft break up or lose some of the functionality is not due to the intrigues of aliens (the Martians swear that they did not shoot ExoMars).

I would like to consider the causes and possible solutions to this planetary problem.

1. The lack of professionalism and incompetence of the performers - earthlings, for the most part, are not taught and accustomed to do their job well. This problem is very serious, and you can talk about it for a long time, but apparently you need to write a separate post. Here you can only say that there are real professionals after all, there should be enough for advanced projects, but there are problems in such projects, so this is not the only thing.
   ')
   
2. Lack of goals to do well / bad management / insufficient investments - this is quite likely in ordinary commercial projects, where the task is to get short-term profit, and not to do well. But this is clearly not about space projects, where the cost of a mistake is too high both in money and reputation, and the development costs, according to some estimates , are 160 times higher than normal commercial development, but also without a guarantee of reliability.
   
   
3. Using unsuitable tools / trying to grind a lens with a hammer — this seems to me to be the main reason and I’ll talk about it later. It is because of the wrong approach to solving problems that honest programmers never say "Yes, it works," but they say, "It seems to work," "Must work."

When earthlings take on the most difficult of the tasks before them, it would be logical to apply the best available tools to solve them.
And this tool is definitely not a human brain , the brain of homo sapiens is just a tool from the “seems to work” series and you shouldn’t be surprised, it evolved for very different tasks, so even the coolest professional can make a stupid mistake on the heap reasons.

Of course, bringing together many good brains, you can improve the result, but without a good tool and all the brains of the planet will not achieve what has already been achieved.

To understand what kind of magic tool it is worth trying to answer questions like “Why don't skyscrapers collapse under their weight or in the wind?”, “How do our spacecraft get to the target in the vast expanses of space?”, “How do we manage to reliably send data via unreliable communication channels? ”,“ Where did reliable encryption methods come from? ”and so on and so forth.

The answer to all these questions is one, this tool is mathematics . Mathematics is the magic of the modern world, for the uninitiated, such artifacts as Zcash or CryptDB , and, as usual, asymmetric encryption looks like magic, although this is only the use of this powerful tool.

In order to say - “Yes, the program works as demanded”, one must have a mathematical proof of this statement, unfortunately I am not an expert in this field, but as far as I know the process of this proof is rather complicated, but this should not be an obstacle for the following reasons:

1. There is no other way, our systems are becoming more complex, the new layers are based on the old ones, but unfortunately this is not a very reliable foundation.
   
   
2. You need to prove small programs ( unix-way ).
   
   
3. It is only necessary to prove that the programs are safety-critical reliability. You can not prove the correctness of the office suite, but the OS microkernel or encryption libraries must be proven.
   
   
4. Prove not necessarily an existing universal software, not necessarily it will be a general-purpose OS, perhaps something simpler, without whistles, but as reliable as possible for medicine, transport, nuclear power plants.
   
   
5. Using strictly mathematical programming languages ​​can reduce the cost of proof ( Haskell ?). Yes, they can be somewhat more complicated than ordinary PLs, but their complexity corresponds to the complexity of the tasks that need to be addressed.
   
   
6. It is not necessary to prove everything at once, but step by step you can build a proven infrastructure for building reliable systems.

Of course, the proof of programs does not relieve us of the need to formulate requirements precisely, but I think this is a solvable task, especially since in some cases (like encryption libraries) the requirements themselves are also formalized.

I think everyone would like to have absolutely reliable software working at nuclear power plants, in medical equipment and similar places.

I will not argue that it was necessary to do this a long time ago, the industry was booming, a lot of things have changed significantly, but today, from my point of view, the industry is mature enough to start putting things in order.

There are new classes of tasks like quantum computers and specialized processors for neural networks, everything is just beginning there. But the development of these industries does not negate the necessity of the classical approach - all have their own tasks.

Earth civilization is already very dependent on the reliability of computer systems, and in order not to flinch at night from the noise of the wings of a flying woodpecker, it is necessary to look for solutions that increase reliability.


Separately, it should be said about neural networks, neural networks are an attempt to replicate the brain with all its pluses and minuses, the solution on neural networks contains the same problems as the human brain, so they should be used only where we do not know how to solve the problem using formal The algorithm works absolutely reliably.

I think that in order for the earth civilization to develop steadily, it is time to think about the reliability of its infrastructure, regarding IT it seems to me like this - you need to select / create a high-level mathematical programming language and start creating completely on it (without hidden sichnyh lib) under the hood their subsequent evidence. It is likely that the hardware architecture of processors must be proved and sharpened for the execution of programs in such a language ( lisp-machines ?).

Who should do this? I don’t know, but the same question could be asked on the proposal of the entire world to write the OS kernel, but Linux is completely written, which means there are options. For example, there is a formally verified seL4 core ( explained in their wiki ) developed by NICTA , if such projects do not become the basis for the digital infrastructure of the future, then humanity will have a chance not to go through the great filter of civilizations (who is sure that the virus will not start a nuclear war?).

UPDATE: In the process of discussion in the comments, an important idea matured: in order to implement verified software in critical areas, it is not necessary to stop the current development, you need to simultaneously create free verified components, and for their readiness to do new things with their help, for example, the above-mentioned seL4 microkernel for embedded needs already, so you need to use it wherever it fits. And work on other components.