You can prove that an algorithm is correct most of the time (yes, halting and decidability but for practical purposes you mostly can).
How do you prove an event driven application is correct?
Make formal verification and provably correct software practical and mainstream
121–130 of 203 posts
Re: Make formal verification and provably correct software practical and mainstream
#122Earlier quoted context omitted.
> The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. The kinds of theorems that we need to prove in software are much more elementary than what mathematicians are proving. I think software engineering can benefit from it long before mathematicians start doing cutting-edge math in it.
Not if you do software the right way. Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ... Furthermore, I don't think cutting-edge math needs a much different approach from cutting-edge software. You need to be able to express your thoughts succinctly, and have the tools to reason about them. It is often said that software verification is different because there is much…
> Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ...
You don't need to verify the entire program for formal verification to be useful. You can adopt it incrementally.
The most common bogus argument I hear against formal verification is that it's impractical to come up with a spec or proof for the entire program, so we might as well not even bother with formal verification at all.
Re: Make formal verification and provably correct software practical and mainstream
#123As the article mentions, formal verification techniques are primarily used today for two things: - Creating secure "core" code -- library functions and kernels and stuff, where the things they're supposed to do are very well-defined. - Verifying specific, narrowly defined properties, like how Rust's borrow checker guarantees that your program doesn't try to write to the same value from two different threads at once.…
I think this sharply discounts the value of the step before the proof which is writing the specification in a formal language/logic. This often surfaces these misunderstandings before a proof is even necessary. That doesn’t guarantee that the spec will be the right one (as you say) but it’s astounding how often just writing it down formally improves the implementation through rigorous thought.
> That doesn’t guarantee that the spec will be the right one (as you say) but it’s astounding how often just writing it down formally improves the implementation through rigorous thought.
But that doesn't have much to do with formal methods. You can achieve the same effect grabbing a colleague and explaining your spec to them, it will trigger the same rigorous thought because you want them to understand you.
Re: Make formal verification and provably correct software practical and mainstream
#124Earlier quoted context omitted.
Looks interesting, perhaps because it seems to be a bit more down to earth than some of the other proposals where you have to derive Whitehead&Russell before you're allowed to use the + operator. But it also seems quite dead. The latest link is from 2012.
It is still alive, it has just moved to github! It is a big language and it can prove useful programs. Apparently, part of the Ethereum 2 specification was verified using it. https://github.com/dafny-lang/dafny I have been learning it and the syntax is close to most C style programming languages. As a software developer this makes it much more approachable than Coq. The proof statements also feel more like the math I…
Thanks. Pretty cool.
Re: Make formal verification and provably correct software practical and mainstream
#125Earlier quoted context omitted.
Not if you do software the right way. Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ... Furthermore, I don't think cutting-edge math needs a much different approach from cutting-edge software. You need to be able to express your thoughts succinctly, and have the tools to reason about them. It is often said that software verification is different because there is much…
> Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ... You don't need to verify the entire program for formal verification to be useful. You can adopt it incrementally. The most common bogus argument I hear against formal verification is that it's impractical to come up with a spec or proof for the entire program, so we might as well not even bother with formal verifica…
Formal verification is just very costly and has diminishing returns. Let's take a CAD program. Which aspects of it would you formally verify? If you are going for the easy parts, those can already be dealt with nicely with static typing and testing, essentially push-button automated verification. If you are going for the interesting parts, you will be doing math, essentially.
Re: Make formal verification and provably correct software practical and mainstream
#126Try the proof assistant Agda without installation directly in your browser:
https://agdapad.quasicoherent.io/
Or Lean: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_g...
Re: Make formal verification and provably correct software practical and mainstream
#127While I laud the goals, I am skeptical of the ability to met them.
I very much believe that there is an industry-wide crisis of terrible software, but I don't believe that it's practical to go directly from "garbage to gold." The path is long, and far from straight.
Best Practices are how engineering disciplines, throughout history, have achieved progress in Quality.
Currently, Best Practices aren't really a "thing," in software development, and it shows. People like Steve McConnell are not really respected, and a general culture of "move fast and break things" is still pervasive. Engineers flit around companies like mayflies, techniques and libraries come and go, and there's an enormous reliance on dependencies with very little vetting. We spend so much time, trying to perfect our tools, without trying to perfect ourselves.
Academics and theorists have been proposing languages, libraries, infrastructure, and management practices that are designed to change lead into gold for decades, yet it never seems to happen.
I have always been a fan of self-Discipline, and the apprenticeship model. That requires a lot of social infrastructure that does not currently exist. It's as old as human history, and absolutely proven to achieve results.
"In theory, there is no difference between theory and practice; while in practice, there is." -Benjamin Brewster
"It is not enough to do your best; you must know what to do, and THEN do your best." -W. Edwards Deming
"The significant problems we face cannot be solved by the same level of thinking that created them." -Albert Einstein
"Everyone thinks of changing the world, but not one thinks of changing himself." -Tolstoy
Re: Make formal verification and provably correct software practical and mainstream
#128Microsoft developed the excellent Code Contracts[1] project. From the user's perpective, tt was a simple class called Contracts with a few methods such as Require(), Ensure() and Invariant()
Underneath the hood it used the Z3 Solver[2], which is both intuitive, flexible and fast. It validated the contracts while coding and highlighted in the Visual Studio IDE when a contract was broken.
You could write something like: Contracts.Requires(x > 5 && y > x);
Which would get translated to a compile time check as well. Unfortunately, Code Contracts has been dead for years now, and it was even removed entirely from .NET[3] due to being hard to maintain, and the verifier stopped working in newer versions of VS.
Luckily, C# developers now have a small taste of contracts due to nullability analysis[4], but even more exciting is that contracts is making its way into C# as a first-level standard[5].
[1] https://www.microsoft.com/en-us/research/project/code-contra...
[2] https://github.com/Z3Prover/z3
[3] https://github.com/dotnet/runtime/issues/20006
[4] https://docs.microsoft.com/en-us/dotnet/csharp/nullable-refe...
Re: Make formal verification and provably correct software practical and mainstream
#129While I laud the goals, I am skeptical of the ability to met them. I very much believe that there is an industry-wide crisis of terrible software, but I don't believe that it's practical to go directly from "garbage to gold." The path is long, and far from straight. Best Practices are how engineering disciplines, throughout history, have achieved progress in Quality. Currently, Best Practices aren't really a "thing,"…
> While I laud the goals, I am skeptical of the ability to met them.
Let's start with the easiest part, and rewrite everything in Rust (or a comparably safe language). We'll need something like this anyway to give our software a workable semantics that's free of UB (at least wrt. the "safe" checked subset). Then we can work on the harder problem of using proof to establish that the unchecked parts do not invoke UB, and that intended specifications are not violated even in the "safe" parts.
Re: Make formal verification and provably correct software practical and mainstream
#130Earlier quoted context omitted.
> Try to prove correctness of a CAD program, for example. Or of a graphics card implementation. Or ... You don't need to verify the entire program for formal verification to be useful. You can adopt it incrementally. The most common bogus argument I hear against formal verification is that it's impractical to come up with a spec or proof for the entire program, so we might as well not even bother with formal verifica…
Formal verification is just very costly and has diminishing returns. Let's take a CAD program. Which aspects of it would you formally verify? If you are going for the easy parts, those can already be dealt with nicely with static typing and testing, essentially push-button automated verification. If you are going for the interesting parts, you will be doing math, essentially.
> Let's take a CAD program. Which aspects of it would you formally verify?
Any large program will contain some smaller components with relatively well-defined behavior. CAD is not my specialty, so I can't really comment on what algorithms are used in that domain. Forgetting about fancy algorithms for a moment, just having a more expressive type system will allow you to express invariants in your code like the fact that array indices are within the relevant bounds, that you never try to pop an empty stack, etc.—everyday programming issues.
For a more concrete example, lately I've been using Coq to formally verify critical properties about a certain type of graph-like data structure I'm using in a system I'm building.
> If you are going for the easy parts, those can already be dealt with nicely with static typing and testing, essentially push-button automated verification.
Most engineers are already writing tests and using static types. Yet, we still have buggy programs.
And just to be clear, the kind of formal verification we're talking about is based on static typing. It's just a more expressive type system than what most programmers are used to.
> If you are going for the interesting parts, you will be doing math, essentially.
You are doing some form of math, but not the kind of cutting edge math that mathematicians do—which was my original point. You are not going to run into the kinds of tricky problems that mathematicians run into with theorem proving software, like universes being too small etc. Most data in software engineering is finite and reasoning about it involves little more than arithmetic and induction (which is just out of reach for mainstream type systems, but not for the kind of type systems used in proof assistants).