Working with verification with Clang/LLVM as we speak. The state of verification is... bleak at the moment.
The math and algorithms are working, and some very smart (and very pleasant, I might add) people are working around the clock, including from e.g. the French Commission for Nuclear Energy.
However, the learning curve is too high and the developer-experience is very poor at the moment. This is a classic case of gaps between research material and usability.
Fortunately, I see this as where software is headed, especially languages people love to tout as being "unsafe", such as C.
The article is exactly right - tests only test the programmer, not the program. Formal verification is The Way, in my opinion.
In a software project with sufficiently complicated features/requirements, I'd imagine the formal specification is likely as complicated as the program itself. There are ways to make the specification language less error prone, but... that's what the software community has already been doing for decades, by inventing new high level programming languages that are easier to read/write and less prone to error.
IMHO the advances we've seen in high level languages in the past couple decades is in a sense equivalent to formal verification (at least verification of lower level languages like C). Heck, a lot of languages compile down into C as an intermediate form. Although we don't usually think of it that way, I'd say they are as close as "a formal specification language for C" as you can realistically hope for. And as an added bonus, it generates "provably equivalent" C code and thus saves you from writing it explicitly.
That said, there might be value in re-writing code again and proving that the two pieces of code are functionally equivalent. I'm not sure this would be an easy sell from a commercial standpoint though... If systems were important enough that that warrants approaches like this, one can always ask _three_ teams to implement a spec separately, and then take the result of the majority...
[+] [-] junon|5 years ago|reply
The math and algorithms are working, and some very smart (and very pleasant, I might add) people are working around the clock, including from e.g. the French Commission for Nuclear Energy.
However, the learning curve is too high and the developer-experience is very poor at the moment. This is a classic case of gaps between research material and usability.
Fortunately, I see this as where software is headed, especially languages people love to tout as being "unsafe", such as C.
The article is exactly right - tests only test the programmer, not the program. Formal verification is The Way, in my opinion.
[+] [-] hnfong|5 years ago|reply
In a software project with sufficiently complicated features/requirements, I'd imagine the formal specification is likely as complicated as the program itself. There are ways to make the specification language less error prone, but... that's what the software community has already been doing for decades, by inventing new high level programming languages that are easier to read/write and less prone to error.
IMHO the advances we've seen in high level languages in the past couple decades is in a sense equivalent to formal verification (at least verification of lower level languages like C). Heck, a lot of languages compile down into C as an intermediate form. Although we don't usually think of it that way, I'd say they are as close as "a formal specification language for C" as you can realistically hope for. And as an added bonus, it generates "provably equivalent" C code and thus saves you from writing it explicitly.
That said, there might be value in re-writing code again and proving that the two pieces of code are functionally equivalent. I'm not sure this would be an easy sell from a commercial standpoint though... If systems were important enough that that warrants approaches like this, one can always ask _three_ teams to implement a spec separately, and then take the result of the majority...
[+] [-] tjalfi|5 years ago|reply
[0] https://news.ycombinator.com/item?id=26629779
[+] [-] macintux|5 years ago|reply
A copy of the original paper from Hoare:
https://www.cs.cmu.edu/~crary/819-f09/Hoare69.pdf
[+] [-] dmolony|5 years ago|reply