I never really got how proofs are supposed to solve this issue. I think that would just move the bugs from the code into the proof definition. Your code may do what the proof says, but how do you know what the proof says is what you actually want to happen?
A formal spec isn't just ordinary source-code by another name, it's at a quite different level of abstraction, and (hopefully) it will be proven that its invariants always hold. (This is a separate step from proving that the model corresponds to the ultimate deliverable of the formal development process, be that source-code or binary.)
Bugs in the formal spec aren't impossible, but use of formal methods doesn't prevent you from doing acceptance testing as well. In practice, there's a whole methodology at work, not just blind trust in the formal spec.
Software developed using formal methods is generally assured to be free of runtime errors at the level of the target language (divide-by-zero, dereferencing NULL, out-of-bounds array access, etc). This is a pretty significant advantage, and applies even if there's a bug in the spec.
> A formal spec isn't just ordinary source-code by another name, it's at a quite different level of abstraction
This is the fallacy people have when thinking they can "prove" anything useful with formal systems. Code is _already_ a kind formal specification of program behavior. For example `printf("Hello world");` is a specification of a program that prints hello world. And we already have an abundance of tooling for applying all kind of abstractions imaginable to code. Any success at "proving" correctness using formal methods can probably be transformed into a way to write programs that ensure correctness. For example, Rust has pretty much done so for a large class of bugs prevalent in C/C++.
The mathematician's wet dream of applying "mathematical proof" on computer code will not work. That said, the approach of inventing better abstractions and making it hard if not impossible for the programmer to write the wrong thing (as in Rust) is likely the way forward. I'd argue the Rust approach is in a very real way equivalent to a formal specification of program behavior that ensures the program does not have the various bugs that plagues C/C++.
Of course, as long as the programming language is Turing Complete you can't make it impossible for the programmer to mistakenly write something they didn't intend. No amount of formalism can prevent a programmer from writing `printf("hello word")` when they intended "hello world". Computers _already_ "do what I say", and "do what I mean" is impossible unless people invent a way for minds to telepathically transmit their intentions (by this point you'd have to wonder whether the intention is the conscious one or the subconscious ones).
> thinking they can "prove" anything useful with formal systems
As I already said in my reply to xmprt, formal methods have been used successfully in developing life-critical code, although it remains a tiny niche. (It's a lot of work, so it's only worth it for that kind of code.) Google should turn up some examples.
> Code is _already_ a kind formal specification of program behavior.
Not really. Few languages even have an unambiguous language-definition spec. The behaviour of C code may vary between different standards-compliant compilers/platforms, for example.
The SPARK Ada language, on the other hand, is unambiguous and is amenable to formal reasoning. That's by careful design, and it's pretty unique. It's also an extremely minimal language.
> `printf("Hello world");` is a specification of a program that prints hello world
There's more to the story even here. Reasoning precisely about printf isn't as trivial as it appears. It will attempt to print Hello world in a character-encoding determined by the compiler/platform, not by the C standard. It will fail if the stdout pipe is closed or if it runs into other trouble. Even a printf call has plenty of complexity we tend to just ignore in day to day programming, see https://www.gnu.org/ghm/2011/paris/slides/jim-meyering-goodb...
> Any success at "proving" correctness using formal methods can probably be transformed into a way to write programs that ensure correctness
You've roughly described SPARK Ada's higher 'assurance levels', where each function and procedure has not only an ordinary body, written in SPARK Ada, but also a formal specification.
SPARK is pretty challenging to use, and there can be practical limitations on what properties can be proved with today's provers, but still, it is already a reality.
> Rust has pretty much done so for a large class of bugs prevalent in C/C++
Most modern languages improve upon the appalling lack of safety in C and C++. You're right that Rust (in particular the Safe Rust subset) does a much better job than most, and is showing a lot of success in its safety features. Programs written in Safe Rust don't have memory safety bugs, which is a tremendous improvement on C and C++, and it manages this without a garbage collector. Rust doesn't really lend itself to formal reasoning though, it doesn't even have a proper language spec.
> The mathematician's wet dream of applying "mathematical proof" on computer code will not work
Again, formal methods aren't hypothetical.
> I'd argue the Rust approach is in a very real way equivalent to a formal specification of program behavior that ensures the program does not have the various bugs that plagues C/C++.
It is not. Safe languages offer rock-solid guarantees that certain kinds of bugs can't occur, yes, and that's very powerful, but is not equivalent to full formal verification.
It's great to eliminate whole classes of bugs relating to initialization, concurrency, types, and object lifetime. That doesn't verify the specific behaviour of the program, though.
> No amount of formalism can prevent a programmer from writing `printf("hello word")` when they intended "hello world"
That comes down to the question of how do you get the model right? See the first PDF I linked above. The software development process won't blindly trust the model. Bugs in the model are possible but it seems like in practice it's uncommon for them to go unnoticed for long, and they are not a showstopper for using formal methods to develop ultra-low-defect software in practice.
> "do what I mean" is impossible unless people invent a way for minds to telepathically transmit their intention
It's not clear what your point is here. No software development methodology can operate without a team that understands the requirements, and has the necessary contact with the requirements-setting customer, and domain experts, etc.
I suggest taking a look at both the PDFs I linked above, by way of an introduction to what formal methods are and how they can be used. (The Formal methods article on Wikipedia is regrettably rather dry.)
I think the reason that formal proofs haven't really caught on is because it's just adding more complexity and stuff to maintain. The list of things that need to be maintained just keeps growing: code, tests, deployment tooling, configs, environments, etc. And now add a formal proof onto that. If the user changes their requirements then the proof needs to change. A lot of code changes will probably necessitate a proof change as well. And it doesn't even eliminate bugs because the formal proof could include a bug too. I suppose it could help in trivial cases like sanity checking that a value isn't null or that a lock is only held by a single thread but it seems like a lot of those checks are already integrated in build tooling in one way or another.
Yes, with the current state of the art, adopting formal methods means adopting a radically different approach to software development. For 'rapid application development' work, it isn't going to be a good choice. It's only a real consideration if you're serious about developing ultra-low-defect software (to use a term from the AdaCore folks).
> it doesn't even eliminate bugs because the formal proof could include a bug too
This is rather dismissive. Formal methods have been successfully used in various life-critical software systems, such as medical equipment and avionics.
As I said above, formal methods can eliminate all 'runtime errors' (like out-of-bounds array access), and there's a lot of power in formally guaranteeing that the model's invariants are never broken.
> I suppose it could help in trivial cases like sanity checking that a value isn't null or that a lock is only held by a single thread
No, this doesn't accurately reflect how formal methods work. I suggest taking a look at the PDFs I linked above. For one thing, formal modelling is not done using a programming language.
You mix up development problem with computational problem.
If you can't use formal proof just because the user can't be arsed to wait where it is supposed to be necessary, then the software project conception is simply not well designed.
As always, the branding of formal methods sucks. As other commentators point out, it isn't technically possible to provide a formal proof that software is correct. And that is fine, because formal software methods don't do that.
But right from the outset the approach is doomed to fail because its proponents write like they don't know what they are talking about and think they can write bug-free software.
It really should be "write software with a formal spec". Once people start talking about "proof" in practice it sounds dishonest. It isn't possible to prove software and the focus really needs to be on the spec.
> It really should be "write software with a formal spec".
The code is already a formal spec.
Unless there are bugs in the language/compiler/interpreter, what the code is essentially formally well defined.
As programming languages get better at enabling programmers to communicate intention as opposed to being a way to generate computer instructions, there's really no need for a separate "spec". Any so called "spec" that is not a programming language is likely not "formal" in the sense that the behavior is unambiguously well defined.
Of course, you might be able to write the "spec" using a formal language that cannot be transformed into machine code, but assuming that the "spec" is actually well defined, then it's just that "compiling" the spec into machine code is too expensive in some way (eg. nobody has written a compiler, it's too computationally hard to deduce the actual intention even though it's well defined, etc.). But in essence it is still a "programming language", just one without a compiler/interpreter.
You can formally prove that it doesn't have certain kinds of bugs. And that's good! But it also is an enormous amount of work. And so, even for life-critical software, the vast majority is not formally proven, because we want more software than we can afford to formally prove.
This is an interesting point that I think a lot of programming can miss.
Proving that the program has no bugs is akin to proving that the program won't make you feel sad. Like ... I'm not sure we have the math.
One of the more important jobs of the software engineer is to look deep into your customer's dreams and determine how those dreams will ultimately make your customer sad unless there's some sort of intervention before you finish the implementation.
Exactly, it's fundamentally impossible. Formal proofs can help with parts of the process, but it can guarantee no bugs in the product. These are the steps of software, and their transitions. It's fundamentally a game of telephone with errors at each step along the way.
What actually would solve the customer's problem -> What the customer thinks they want -> What they communicate that they want -> What the requirements collector hears -> What the requirements collector documents -> How the implementor interprets the requirements -> What the implementor designs/plans -> What the implementor implements.
Formal proofs can help with the last 3 steps. But again that's assuming the implementor can formalize every requirement they interpreted. And that's impossible as well, there will always be implicit assumptions about the running environment, performance, scale, the behavior of dependent processes/APIs.
It helps with a small set of possible problems. If those problems are mission-critical then absolutely tackle them, but there will never be a situation where it can help with the first 5 steps of the problem, or with the implicit items in the 6th step above.
Even formally proved code can have bugs. If your requirement is wrong is the obvious thing. I don't work with formal proofs (I want to, I just don't know how), but I'm given to understand they have other real world limits that make them sometimes have other bugs.
Or perhaps you'll prove it from first principles. Although if turns out to be difficult, that's okay. Somebody mentioned something about systems being either complete or consistent but never both. Some things can be true but not proveably so. Can't quite remember who it was though.
Gödel's really was a rather unique mind, and the story of his death is kind of sad.. but I wonder if it takes such a severe kind of paranoia to look for how math can break itself, especially during that time when all the greatest mathematicians were in pursuit of formalizing a complete and consistent mathematics.
No. It merely prevents you from confirming every arbitrarily complex proof. Incompleteness is more like: I give you a convoluted mess of spaghetti code and claim it computes prime numbers and I demand you try to prove me wrong.
There are well-formed statements that can be proved but which assert that its godelized value represents a non-provable theorem.
Therefore, you must accept that it and its contradiction are both provable (leading to an inconsistent system), or not accept it and now there are provable theorems that cannot be expressed in the system.
Furthermore, that this can be constructed from anything with base arithmetic and induction over first-order logic (Gödel's original paper included how broadly it could be applied to basically every logical system).
The important thing to note is that it doesn't have anything to do with truth or truth-values of propositions. It breaks the fundamental operation of the provability of a statement.
And, since many proofs are done by assuming a statement's inverse and trying to prove a contradiction, having a known contradiction in the set of provable statements can effectively allow any statement to be proven. Keeping the contradiction is not actually an option.
I jest, but that should be the gold standard for anything life-critical and good to have for mission-critical software. Alas, we're not there yet.