3 ms·

> verifying code correctness is impossible Somehow, taking into account the state of our industry, yes. But this is not an absolute truth. I mean, we do have

> verifying code correctness is impossible Somehow, taking into account the state of our industry, yes. But this is not an absolute truth. I mean, we do have the theoretical frameworks and even tools to come with solutions that allow to proof that code is correct. It’s just that mapping this "know how" with the "how to deal with the expected flow rate feature" is very uncommon.

tpm 2y ago
It is an absolute truth in the sense that it is true for all code that was not specifically written to be formally proven correct. So, given an arbitrary piece of code, it's impossible to verify it (because of the halting problem).
- skydhash 2y ago
  It's not impossible to verify it, it's impossible to automatically verify it with another program. Other issues are the underlying abstract machine (which can have its own bugs) and the surrounding environment (you either need to assert or/and sanitize your inputs).
- versteegen 2y ago
  Those assertions are a long way off absolutely true! The undecidability of Turing machines in general doesn't say you can't reason about any programs, as you seem to claim, it says there exists programs which have unverifiable behaviour. (Although the proof provides unnatural examples, in practice simple recursive mathematical functions such as the Collatz conjecture will probably always be beyond automated analysis.) Of course software that was not written with verification in mind can be verified correct, provided it doesn't contains things such as an interpreter or complex conditional recursion. There are static analysis tools for analysing programs in languages such as C++ which make use of ATPs (automated theorem provers). For example, most of zlib has been proven correct using Coq. Yes, verification of the entirety of complex programs is in general impossible, but parts of them can still be verified. It's the most common use of ATPs, and an active area of research!
n4r9 2y ago
> tools to come with solutions that allow to proof that code is correct I may be misunderstanding, but isn't part of the problem that these tools are themselves written in code and therefore subject to bugs?
- superidiot1932 2y ago
  There are verified compilers such as the compcert compiler and also ways to verify that a given binary does in fact correctly implement an specification
- agentultra 2y ago
  This is addressed by the de Bruijn Criterion. The essential idea is that a small number of "trusted" rules should be enough to satisfy even the largest proofs. You have to keep the number of rules small enough that they can be reviewed and understood by humans so that you can trust the proofs verified by the kernel.
  - n4r9 2y ago
    That probably helps to reduce the occurrence of issues, but I feel you are still ultimately relying on the correctness of proof assistants like Coq. And I am sure that bugs are occasionally found in Coq!
    - agentultra 2y ago
      Indeed it does happen and it's unavoidable. You have to pick your axioms from somewhere and sometimes we pick the wrong ones or we find errors in our definitions. There's no "complete" or "perfect" system.

tpm 2y ago

It is an absolute truth in the sense that it is true for all code that was not specifically written to be formally proven correct. So, given an arbitrary piece of code, it's impossible to verify it (because of the halting problem).

skydhash 2y ago
It's not impossible to verify it, it's impossible to automatically verify it with another program. Other issues are the underlying abstract machine (which can have its own bugs) and the surrounding environment (you either need to assert or/and sanitize your inputs).
versteegen 2y ago
Those assertions are a long way off absolutely true! The undecidability of Turing machines in general doesn't say you can't reason about any programs, as you seem to claim, it says there exists programs which have unverifiable behaviour. (Although the proof provides unnatural examples, in practice simple recursive mathematical functions such as the Collatz conjecture will probably always be beyond automated analysis.) Of course software that was not written with verification in mind can be verified correct, provided it doesn't contains things such as an interpreter or complex conditional recursion. There are static analysis tools for analysing programs in languages such as C++ which make use of ATPs (automated theorem provers). For example, most of zlib has been proven correct using Coq. Yes, verification of the entirety of complex programs is in general impossible, but parts of them can still be verified. It's the most common use of ATPs, and an active area of research!

n4r9 2y ago

> tools to come with solutions that allow to proof that code is correct I may be misunderstanding, but isn't part of the problem that these tools are themselves written in code and therefore subject to bugs?

superidiot1932 2y ago
There are verified compilers such as the compcert compiler and also ways to verify that a given binary does in fact correctly implement an specification
agentultra 2y ago
This is addressed by the de Bruijn Criterion. The essential idea is that a small number of "trusted" rules should be enough to satisfy even the largest proofs. You have to keep the number of rules small enough that they can be reviewed and understood by humans so that you can trust the proofs verified by the kernel.
- n4r9 2y ago
  That probably helps to reduce the occurrence of issues, but I feel you are still ultimately relying on the correctness of proof assistants like Coq. And I am sure that bugs are occasionally found in Coq!
  - agentultra 2y ago
    Indeed it does happen and it's unavoidable. You have to pick your axioms from somewhere and sometimes we pick the wrong ones or we find errors in our definitions. There's no "complete" or "perfect" system.