6 ms·

A few years back, I was trying to find out how to reduce mistakes in the programs I write. I got introduced to Lamport's TLA+ for creating formal specification

A few years back, I was trying to find out how to reduce mistakes in the programs I write. I got introduced to Lamport's TLA+ for creating formal specifications, thinking of program behaviors in state machines. TLA+ taught me about abstraction in a clear manner. Then I also discovered the book series "software foundations", which uses the Coq proof assistant to build formally correct software. The exercises in this book are little games and I found them quite enjoyable to work through. https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/

samvher 3y ago
I had the same positive experience with Software Foundations. There is another book somewhat derived from it (if I understand correctly) using Agda instead of Coq: https://plfa.github.io/ https://plfa.github.io/ I haven't had the chance to go through it yet, but it's on my list - I think Agda (and as mentioned by another commenter, Idris) is likely to feel more like a programming language than Coq.
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.
deleted 3y ago
[deleted]
aeonik 3y ago
Have you looked into Idris2 at all. While looking into these theorum provers, it always felt like they had an impedance mismatch with normal programming. Idris2 portends to a general purpose language that also has a more advanced type system for the theorum proving. https://github.com/idris-lang/Idris2 https://github.com/idris-lang/Idris2
- atomicnature 3y ago
  That's interesting; no I wasn't aware of it. Will check it out sometime, thanks.
  - iso8859-1 3y ago
    There's a list of packages here: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STATUS.md https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...

samvher 3y ago

I had the same positive experience with Software Foundations. There is another book somewhat derived from it (if I understand correctly) using Agda instead of Coq: https://plfa.github.io/ https://plfa.github.io/ I haven't had the chance to go through it yet, but it's on my list - I think Agda (and as mentioned by another commenter, Idris) is likely to feel more like a programming language than Coq.

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.

deleted 3y ago

[deleted]

aeonik 3y ago

Have you looked into Idris2 at all. While looking into these theorum provers, it always felt like they had an impedance mismatch with normal programming. Idris2 portends to a general purpose language that also has a more advanced type system for the theorum proving. https://github.com/idris-lang/Idris2 https://github.com/idris-lang/Idris2

atomicnature 3y ago
That's interesting; no I wasn't aware of it. Will check it out sometime, thanks.
- iso8859-1 3y ago
  There's a list of packages here: https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STATUS.md https://github.com/stefan-hoeck/idris2-pack-db/blob/main/STA...