ioseb 🇬🇪🇺🇦

Formal verification of correctness will never be a worthy industry practice.🚷 Software becomes obsolete much faster than it becomes correct.🚮 Statically-checked "correctness" is just a questionable tactic to squeeze money out of the industry.🧑‍🔧🔫🕵️ Here is why.⬇️ There is indeed a niche for formal verification. Static formal verification somewhat works for critical components and delicate parts of bigger systems. For example: cryptography protocols, data transformation algorithms, compilers, and parts of SCADA systems. However, even in this niche, full verification of a relatively big application is not possible. The real world is much more chaotic and disorganized. New requirements are coming constantly, and some of them contradict what was already done and was already proven. Haskellers are probably the biggest cult of believers in holy correctness from all the programming communities. They even believe that "correctness" is a scientifically defined term that cannot have any other meaning. "If you don't know what correctness is, - they say, - this doesn't mean nobody knows. Go and read the papers". Sure, because scientific papers are the only source of truth out there. You have no permission to question it, and you have no right to define it yourself unless you write a paper. Am I correct? What haskellers (and formal verification folks) call "correctness" is one of the four: ▪️ Correctness of data structures and data models. A structure has some proven invariant that is statically checked by the compiler. For example, a fixed-length array: type FirstName = Vector 10 Char However, this has nothing to do with the correctness of meaning. This is formally correct but meaningless: john :: FirstName john = " J hn o" ▪️ Correctness of algorithms. Why not prove that the `max` function gives you a maximum of the two numbers. Sure. Now formally prove that my neural network algorithm for image recognition is correct, i.e. produces meaningful results. ▪️ Correctness of languages. "If a language is proven to be correct, the code will be correct, too." This misleading idea has circulated across programming language communities for years. The sad truth is that it's impossible to disallow writing meaningless code no matter how much it is formally verified. The problem here is that this "correctness" has nothing to do with meaning. "Correctness" here is mostly a mechanical term: given a narrow set of preconditions, prove what can be proven, no matter that your model doesn't reflect the complexities of the real world. Moreover, given vague requirements, formal verification folks often prove things that are wrong from the domain point of view. It's statically correct, who cares it's meaningless. Eventually, the proofs will be fixed, and folks feel no shame for that. This is a job security practice anyway, and nobody will punish them. These folks are untouchable and highly respected. Nassim Taleb once said: "For real people, if something works in theory, but not in practice, it doesn't work. For academics, if something works in practice, but not in theory, it doesn't exist." The notion of meaning doesn't exist in theory because it is undefinable. It cannot be proven. But it does exist in practice and can be verified with tests. So why formal proofs won't become a major tool in the industry? ▪️ Formal verification is extremely expensive. These folks demand a high salary for their work ($250K+ net) while their results are questionable at least. ▪️ It is extremely narrow. You need a formally defined environment to construct proofs. Formalizing real domains is nearly impossible due to their complexity and constantly changing requirements. ▪️ It is extremely difficult. Formal verification is Math. Constructing formal proofs is as difficult as discovering Math truths. ▪️ Just because it's Math, it will never dominate the industry. Software developers are not lazy, they are not stupid to do this. Formal verification is just a vastly different profession. (I don't believe that AI will handle this for us, either.) Haskell people love discussing correctness techniques and formal verification in general. But even in Haskell, formal proofs failed to become a common practice. "Correctness" is a cult in Haskell the same way as " performance" in C++. Formal verification is a niche to these niche languages. On the industry scale, it's slightly above the noise level. Static typing didn't even win the battle over the industry. Dynamic languages top the programming language charts. To formal verification folks, dynamic languages don't exist because they work in practice but not in theory. However, the industry is wise, and it sees no commercial benefit in formal verification. This is the proof of proofs to be nearly useless.

When you finish a PhD in computer science, they take you to a special room and explain that you must never use recursion in real life. Its only purpose is to make programming hard for undergrads.

Volodymyr Zelensky address to tens of thousands of Georgians gathered to support Ukraine!

Watch this. And every time Russia says it’s not deliberately killing civilians, watch it again.