5 ms·

Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs)

by Genbox 3y ago

Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model. C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead. The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5]. [1] https://www.microsoft.com/en-us/research/project/code-contracts/ https://www.microsoft.com/en-us/research/project/code-contra... [2] https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [3] https://github.com/microsoft/CodeContracts https://github.com/microsoft/CodeContracts [4] https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny [5] https://github.com/dotnet/csharplang/issues/105 https://github.com/dotnet/csharplang/issues/105

jerf 3y ago
"Code correctness is a lost art." No, it really isn't. It's doing better now than it ever has... and I mean all the negative implications of that. It was not an art that was ever "found" in the sense you mean.
kccqzy 3y ago
Formal verification is often not the best tool for ensuring code correctness from an ROI perspective. Things like unit tests (including property based tests) and ensuring 100% code coverage often achieve adequate results with less effort.
- jlouis 3y ago
  The key point is that most software don't need correctness to the level formal verification provides. There's a subset of software however, for which there's no substitute for a formal verification process.
  - aSanchezStern 3y ago
    Additionally, formal verification usability is an area of constant research, and the set of software for which it is the best ROI increases over time.
- pfdietz 3y ago
  If you can specify your program (or a part of it) well enough to prove it correct, you can also use that specification for property-based testing.
mjburgess 3y ago
The issue is that modern software fails because it's part of a complex system with many moving parts, rather than, it is inherently complex at the source-level. Certain sorts of algorithmically complex development (games, cars, medical hardware, etc.) would benefit from a 'closed-world verification' -- but that's not most software, and they have alternatives. 'Code correctness', including unit testing, ends up being a big misdirection here. What you need is comprehensive end-to-end tests, and instrumentation to identify where failures occur in that end-to-end. The effort to source-level-check source-level-code is largely a huge waste of time and creates an illusion of reliability which rarely exists.
- mrkeen 3y ago
  Strong disagree. > The issue is that modern software fails because it's part of a complex system with many moving parts, rather than, it is inherently complex at the source-level. The choice to run a system as many different moving parts is a decision taken by the team in order to avoid failure. > Certain sorts of algorithmically complex development -- but that's not most software It's all software. > 'Code correctness', including unit testing, ends up being a big misdirection here. What you need is comprehensive end-to-end tests, and instrumentation to identify where failures occur in that end-to-end. No and no. I have comprehensive end-to-end tests. They take forever, don't fit into RAM (for some services I need to run them on my home PC because my work laptop only has 16GB), and most importantly: they show that the code is not correct. Now I have to change incorrect code to correct code (while not breaking any public interfaces. I wish my predecessors did not put incorrect code into the live system.
  - snovv_crash 3y ago
    Tests only show that it is correct for the sets of values and code paths you exercise. It's quite possible for other aspects to be incorrect, and this is what theorem provers like Coq help with.
    - charcircuit 3y ago
      If you have an incomplete or buggy specification Coq won't actually prove the absence of bugs.
throwalean 3y ago
Note that the Z3 SMT solver was written by Leonardo de Moura, who also is the lead dev of Lean 4. Not a coincidence (-; Lean 4 seems to be used in production at AWS: https://github.com/cedar-policy/cedar-spec/pull/138 https://github.com/cedar-policy/cedar-spec/pull/138
pjmlp 3y ago
Or using F* and then generate F# code, https://www.fstar-lang.org/ https://www.fstar-lang.org/
gmadsen 3y ago
Ada is gaining popularity in safety critical systems
- gilcot 3y ago
  Ada/SPARK is already popular in safety critical systems

by Genbox 3y ago

jerf 3y ago

"Code correctness is a lost art." No, it really isn't. It's doing better now than it ever has... and I mean all the negative implications of that. It was not an art that was ever "found" in the sense you mean.

kccqzy 3y ago

Formal verification is often not the best tool for ensuring code correctness from an ROI perspective. Things like unit tests (including property based tests) and ensuring 100% code coverage often achieve adequate results with less effort.

jlouis 3y ago
The key point is that most software don't need correctness to the level formal verification provides. There's a subset of software however, for which there's no substitute for a formal verification process.
- aSanchezStern 3y ago
  Additionally, formal verification usability is an area of constant research, and the set of software for which it is the best ROI increases over time.
pfdietz 3y ago
If you can specify your program (or a part of it) well enough to prove it correct, you can also use that specification for property-based testing.

mjburgess 3y ago

The issue is that modern software fails because it's part of a complex system with many moving parts, rather than, it is inherently complex at the source-level. Certain sorts of algorithmically complex development (games, cars, medical hardware, etc.) would benefit from a 'closed-world verification' -- but that's not most software, and they have alternatives. 'Code correctness', including unit testing, ends up being a big misdirection here. What you need is comprehensive end-to-end tests, and instrumentation to identify where failures occur in that end-to-end. The effort to source-level-check source-level-code is largely a huge waste of time and creates an illusion of reliability which rarely exists.

mrkeen 3y ago
Strong disagree. > The issue is that modern software fails because it's part of a complex system with many moving parts, rather than, it is inherently complex at the source-level. The choice to run a system as many different moving parts is a decision taken by the team in order to avoid failure. > Certain sorts of algorithmically complex development -- but that's not most software It's all software. > 'Code correctness', including unit testing, ends up being a big misdirection here. What you need is comprehensive end-to-end tests, and instrumentation to identify where failures occur in that end-to-end. No and no. I have comprehensive end-to-end tests. They take forever, don't fit into RAM (for some services I need to run them on my home PC because my work laptop only has 16GB), and most importantly: they show that the code is not correct. Now I have to change incorrect code to correct code (while not breaking any public interfaces. I wish my predecessors did not put incorrect code into the live system.
- snovv_crash 3y ago
  Tests only show that it is correct for the sets of values and code paths you exercise. It's quite possible for other aspects to be incorrect, and this is what theorem provers like Coq help with.
  - charcircuit 3y ago
    If you have an incomplete or buggy specification Coq won't actually prove the absence of bugs.

throwalean 3y ago

Note that the Z3 SMT solver was written by Leonardo de Moura, who also is the lead dev of Lean 4. Not a coincidence (-; Lean 4 seems to be used in production at AWS: https://github.com/cedar-policy/cedar-spec/pull/138 https://github.com/cedar-policy/cedar-spec/pull/138

pjmlp 3y ago

Or using F* and then generate F# code, https://www.fstar-lang.org/ https://www.fstar-lang.org/

gmadsen 3y ago

Ada is gaining popularity in safety critical systems

gilcot 3y ago
Ada/SPARK is already popular in safety critical systems