Since there is often a misconception that formally verified software must be absolutely free from problems,
from the conclusion of the paper: "Extensive testing on formally verified software is necessary for at least two reasons.
First, the formal specification may not guarantee all the properties expected
by users, but only critical ones (e.g. no miscompilation for CompCert). Second,
critical bugs may still remain, because the formal specification might not exactly
fit reality. However, in this case, critical bugs are in the—much smaller and
simpler—[trusted computing base]"
"Formally verified software" means that some portion of the software's expected behavior has been rendered as a proposition, and that proposition has been proven correct using some kind of proof assistant or theorem-proving software that we assume correctly validates the proof of the proposition. Bugs can exist in three places, then:
1. Within the theorem-proving software.
2. Within the proposition itself.
3. Within the portions of the code that are not formally verified.
We generally have good reason to suspect bugs in (1) are almost nonexistent. Bugs in (2) and (3) are relatively common, but (3) is no different from the bugs present in software with no formal verification.
A lot of modern theorem-proving research lies in helping people to address bugs in (2) by making propositions easier to write and verify, and in (3) through the same mechanism (because then we can formally verify a greater portion of the software).
> "Formally verified software" means that some portion of the software's expected behavior has been rendered as a proposition, and that proposition has been proven correct using some kind of proof assistant or theorem-proving software that we assume correctly validates the proof of the proposition.
All programs that don't contain undefined behavior satisfy this (in an annoying tautological way) because all programs are proofs of themselves. So the thing you're getting paid for, if you are, is to ask the right questions of your theorem prover (which may be a Python interpreter).
A compiler is a theorem prover, sure, but compilers vary in terms of expressiveness of the propositions it is capable of proving (a Python interpreter would be a very weak theorem prover ;) )
Consider: is there an equivalent concept of Turing Completeness for compilers with respect to computational propositions?
I know what you're saying, but there's a difference between "the expected behavior has been rendered as a proposition" (what I said) and "the expected behavior corresponds with a proposition" (what you're saying).
To "render something as a proposition" means for it to be literally written down in the terms of formal logic. Writing a program in Python doesn't generally constitute this form of expression, but writing a proof of a Python program would.
Thanks for posting this, Dan! It's not usually the sort of thing that gets traction here but I found it a wonderful read, even starting just from the shock of the problem, “You spent all this time proving correctness and it's still not correct.”
Rich Hickey has a similar fun challenge in Simple Made Easy, he addresses the audience:
> A lot of people, as soon as they hear the words “reason about” [programs] they're like, “Oh my God, are you saying that you have to be able to prove programs?” I am not. I don't believe in that. I don't think that's an objective. I'm just talking about informal reasoning, the same kind of reasoning we use every day to decide what we're going to do. We do not take out category theory—we actually can reason without it, thank goodness. So what about the other side?
> There's two things you do with the future of your software. One is, you add new capabilities. The other thing is, you fix the ones you didn't get done so well. And I like to ask this question: What's true of every bug found in the field?
> “Someone wrote it—it got written?” — [eyeroll] Got written, yes, what's a more interesting fact about it?
> It passed the type checker! What else did it do? [Laughs, a couple things shouted]...It passed all the tests. Okay! So now what do you do?
> Right. I think we're in this world that I like to call guard-rail programming. It's really, really sad. We're like, "I can make change 'cause I have tests." Who does that? Who drives their car around banging against the guard-rails like “Whoa, I'm glad I've got these guard rails because I'd never make it to the show on time!” right? And—and do the guard rails help you get to where you want to go? Do they guide you places? No—there's guard rails everywhere, they don't point your car in any particular direction. So again, we're going to need to be able to think about our program, it's going to be critical, all of our guard rails will have failed us when we have a problem.
I really don’t understand how logophobic most programmers, even obviously very bright ones like Mr. Hickey, are.
I had an insight that only partially explains the phenomenon. American programmers, and of course Americans are the cultural standard for the supermajority of the programming world, are obsessively concerned with success in the marketplace. Even free software projects are prone to chasing users. And, as anyone can see, correctness is of virtually no importance to success in the marketplace. What determines commercial success is a different property called pleasantness. And thus it follows that we shouldn’t be surprised that most programmers have no use for rigorous logical reasoning.
There are of course those who enjoy making things unnecessarily complicated to revel in their own cleverness at being able to comprehend their complex creations, but I don’t find their existence to be sufficiently explanatory.
As an american programmer, I don't think you have it exactly correct (though I think you're getting close).
You're right that correctness isn't what I'm shooting for. Pleasantness is important only when the end user is also the one making the decision to use software (so roughly 0% of b2b sales), additionally pleasantness is only important once you've hit a certain floor on another metric, which is generally what I'm actually shooting for.
Usefulness is that metric. That is to say, the ability to use a piece of software to accomplish a practical task. This is, generally speaking, completely orthogonal to correctness, so long as the program is not so incorrect that it doesn't work at all.
The majority of my day is spent implementing business logic that has been decided by fiat by human beings and cannot be logically deduced. Additionally, it is subject to change by human fiat, and the new decision will be correct by definition, even if there are enough special cases that the truth table for the program may be as long as the actual program itself. This gronky business logic is where >80% of my bugs come from (assuming I'm working in a language that manages memory for me).
Proving things about the system doesn't seem particularly useful in that environment. Unless you can figure out how to prove that the VP of accounting is willing to accept a particular risk, or that a governance panel will sign off on a particular change. Political posturing in meetings and interviewing end users and teams working on parallel systems for undocumented requirements/changes my team wasn't told about offer higher ROI.
I think you're basically correct and certainly nothing you say is wrong.
I construe pleasantness a little more broadly. The pleasure target for b2b software isn't the people using it, it's the people signing the purchase orders. And for some reason those people find execrable garbage like a certain extraordinarily slow and wildly overcomplicated project management package that's extremely popular in "the enterprise" pleasant enough to sign giant checks for, to give just one example. I think with that semantic modification we appear to be pretty much on the same page?
Additionally, I've shared some of those insights you mention. I would go a little bit farther and say that actually formally stating those from-the-heavens requirements would improve software quality and possibly even increase pleasantness for the principals in question, that is at least supposing they actually know what it is that they want. A hard "ask" I know.
> I would go a little bit farther and say that actually formally stating those from-the-heavens requirements would improve software quality and possibly even increase pleasantness for the principals in question
Do you think so? It seems to me that they change with little to no warning, and so long as the business is willing to pay for the change, I can't see anything about them being objectively wrong.
Is the value just calling out the things that are most likely to change in a single place?
Formally specifying requirements earlier often reveals inconsistencies and limitations that otherwise only users will reveal in acceptance testing or after deployment.
This generalization has no merit. There's a very wide range of American software, from the formally verified Rust programming language to some Javascript shitlibs. Stanford and Berkeley are home to some very famous formalization efforts.
If anything, I find logically coherent software to be more pleasant (Rust) than something shitty (Python).
And if anything, commercial success seems to be inversely proportional to "pleasantness"
Americans also mostly don't study programming language theory (PLT) (unless they are lucky enough to attend e.g. Carnegie Mellon). A lot of the focus is on algorithms - which is a great shame. The majority of programmers will be consuming/creating APIs and abstractions, not implementing algorithms. PLT would be much more helpful here.
I am not American, I am not obsessed with success in the marketplace, but I like code that actually do something, even if it is just for fun and I am the only one using it, with no hope of profit.
I am not against formal logic, in fact, I am probably more interested by it than most of my fellow programmers, but that's not my main focus of interest. If it was my passion, I would probably have gone for a maths PhD or something like that. No, I code to make the computer do cool stuff and formal analysis may be fun for some time but it quickly gets in the way.
On a more professional note, I code so that my company can make money and pay me, my company need users who pay to make money, therefore, I code to chase users. Proven software is expensive and very few users need that much, so we don't do it.
So if most programmers don't find it fun because they are more makers than scholars and it doesn't really help making money, then it is no surprise that it isn't done often.
> No, I code to make the computer do cool stuff and formal analysis may be fun for some time but it quickly gets in the way.
I agree with the spirit of your comment. I want to add that the defining characteristic of becoming proficient at a technique is that it no longer gets in the way. Touch typing is a good example: when you totally lack proficiency hunt and peck is actually faster. In fact I’ve seen people get up to around 30-50 wpm that way. Having to constantly rehome and remember where the keys are and learn the muscle memory definitely “gets in the way” at first. I think you’ll find if you take the necessary hours that once you achieve proficiency doing things like constructing a nontrivial loop without using an invariant and variant will be considerably more and not less cumbersome.
That said, for exploratory programming, which a lot of professional work frankly is, I don’t find it particularly helpful to worry about proofs until I have a solid grasp on what it is I might want to prove.
Exactly. Guardrails absolutely guide you places if your steering wheel doesn't quite work right. I think that's an apt analogy for modern programming languages.
You rarely need to implement something that has a full testsuite/proof already. You're typically building something new, which means that if you write tests/proofs for it, those are also new code which means they might also be wrong.
Automated tests aren't all that useful to make sure that the code you just wrote does the right thing. People can and do use informal manual testing for that, plus careful crafting and review of the code.
Where automated tests really shine is in preventing your shiny new PR from accidentally messing up the feature you implemented a month ago.
Yes, tests can be wrong. They are still useful for the above, though.
Of course, that is also a useful metaphor here. They do guide you places, and prevent you from making any slight changes to your route. And make it so one stuck train blocks the line.
I find Rich Hickey's talks to present interesting ideas, though I don't like how he presents his ideas. He promotes his ideas, not by arguing for them and pointing out their benefits, but by making fun of opposing viewpoints. Oftentimes, these rebuttals contain little or no actual argumentation, but are rather just full of rhetorical devices.
Take the above, for example. If were to change the metaphor and say: "you know what's true about every fatal car accident where everyone was wearing a seatbelt? Everyone was wearing a seatbelt!" This is the _identical_ rhetorical argument that was made above, but when phrased this way it becomes obvious that it makes no argument.
But that’s actually lends great support to his point! Seatbelts are insufficient. That’s why we have traffic control and licensing and occasionally guard rails. If the only safety for vehicles was seatbelts, it would be quite reasonable to point out that all accidents involved seatbelts.
However, it is irresponsible to present facts without sufficient additional context in order to avoid leading an audience to a faulty conclusion. There is such a thing a misleading an audience by omission and to do so purposefully is dishonest.
I'm not sure the argument you are extracting here is the right one? Traffic control and licensing also don't prevent all accidents, either. You'd need to look into numbers to make an argument.
And by the way, you don't necessarily want accidents to go to zero either. If we wanted that, that would be trivial to achieve: just ban driving. What we want to achieve is a particular trade-off between costs and benefits. In practice we behave as-if human life has a rather finite value, and trade off against it when making traffic decisions.
But there's a difference between saying "you know what's true about every fatal car accident where everyone was wearing a seatbelt? Everyone was wearing a seatbelt!" I could then continue, "this means that seatbelts aren't 100% safety devices. Yes, they save lives, but it's still important to drive safely _and_ we're still on the lookout for better safety devices."
However, Rich Hickey's talk was the equivalent of "you know what's true about every fatal car accident where everyone was wearing a seatbelt? Everyone was wearing a seatbelt! [Laughs] Thus seatbelts suck."
When I saw that lecture, my takeaway was basically your example- we have some tools which help, but they are insufficient. In my experience, there are certainly developers who turn their brains off and rely exclusively on tests or code review.
> Source semantics mismatch: the C language is surprisingly complicated, and its semantics as
formally defined in CompCert may diverge from the informal one defined in the standard, or in CompCert’s manual.
33 comments
[ 6.4 ms ] story [ 99.5 ms ] thread"Formally verified software" means that some portion of the software's expected behavior has been rendered as a proposition, and that proposition has been proven correct using some kind of proof assistant or theorem-proving software that we assume correctly validates the proof of the proposition. Bugs can exist in three places, then:
1. Within the theorem-proving software. 2. Within the proposition itself. 3. Within the portions of the code that are not formally verified.
We generally have good reason to suspect bugs in (1) are almost nonexistent. Bugs in (2) and (3) are relatively common, but (3) is no different from the bugs present in software with no formal verification.
A lot of modern theorem-proving research lies in helping people to address bugs in (2) by making propositions easier to write and verify, and in (3) through the same mechanism (because then we can formally verify a greater portion of the software).
All programs that don't contain undefined behavior satisfy this (in an annoying tautological way) because all programs are proofs of themselves. So the thing you're getting paid for, if you are, is to ask the right questions of your theorem prover (which may be a Python interpreter).
Consider: is there an equivalent concept of Turing Completeness for compilers with respect to computational propositions?
To "render something as a proposition" means for it to be literally written down in the terms of formal logic. Writing a program in Python doesn't generally constitute this form of expression, but writing a proof of a Python program would.
Rich Hickey has a similar fun challenge in Simple Made Easy, he addresses the audience:
> A lot of people, as soon as they hear the words “reason about” [programs] they're like, “Oh my God, are you saying that you have to be able to prove programs?” I am not. I don't believe in that. I don't think that's an objective. I'm just talking about informal reasoning, the same kind of reasoning we use every day to decide what we're going to do. We do not take out category theory—we actually can reason without it, thank goodness. So what about the other side?
> There's two things you do with the future of your software. One is, you add new capabilities. The other thing is, you fix the ones you didn't get done so well. And I like to ask this question: What's true of every bug found in the field?
> “Someone wrote it—it got written?” — [eyeroll] Got written, yes, what's a more interesting fact about it?
> It passed the type checker! What else did it do? [Laughs, a couple things shouted]...It passed all the tests. Okay! So now what do you do?
> Right. I think we're in this world that I like to call guard-rail programming. It's really, really sad. We're like, "I can make change 'cause I have tests." Who does that? Who drives their car around banging against the guard-rails like “Whoa, I'm glad I've got these guard rails because I'd never make it to the show on time!” right? And—and do the guard rails help you get to where you want to go? Do they guide you places? No—there's guard rails everywhere, they don't point your car in any particular direction. So again, we're going to need to be able to think about our program, it's going to be critical, all of our guard rails will have failed us when we have a problem.
I had an insight that only partially explains the phenomenon. American programmers, and of course Americans are the cultural standard for the supermajority of the programming world, are obsessively concerned with success in the marketplace. Even free software projects are prone to chasing users. And, as anyone can see, correctness is of virtually no importance to success in the marketplace. What determines commercial success is a different property called pleasantness. And thus it follows that we shouldn’t be surprised that most programmers have no use for rigorous logical reasoning.
There are of course those who enjoy making things unnecessarily complicated to revel in their own cleverness at being able to comprehend their complex creations, but I don’t find their existence to be sufficiently explanatory.
You're right that correctness isn't what I'm shooting for. Pleasantness is important only when the end user is also the one making the decision to use software (so roughly 0% of b2b sales), additionally pleasantness is only important once you've hit a certain floor on another metric, which is generally what I'm actually shooting for.
Usefulness is that metric. That is to say, the ability to use a piece of software to accomplish a practical task. This is, generally speaking, completely orthogonal to correctness, so long as the program is not so incorrect that it doesn't work at all.
The majority of my day is spent implementing business logic that has been decided by fiat by human beings and cannot be logically deduced. Additionally, it is subject to change by human fiat, and the new decision will be correct by definition, even if there are enough special cases that the truth table for the program may be as long as the actual program itself. This gronky business logic is where >80% of my bugs come from (assuming I'm working in a language that manages memory for me).
Proving things about the system doesn't seem particularly useful in that environment. Unless you can figure out how to prove that the VP of accounting is willing to accept a particular risk, or that a governance panel will sign off on a particular change. Political posturing in meetings and interviewing end users and teams working on parallel systems for undocumented requirements/changes my team wasn't told about offer higher ROI.
I construe pleasantness a little more broadly. The pleasure target for b2b software isn't the people using it, it's the people signing the purchase orders. And for some reason those people find execrable garbage like a certain extraordinarily slow and wildly overcomplicated project management package that's extremely popular in "the enterprise" pleasant enough to sign giant checks for, to give just one example. I think with that semantic modification we appear to be pretty much on the same page?
Additionally, I've shared some of those insights you mention. I would go a little bit farther and say that actually formally stating those from-the-heavens requirements would improve software quality and possibly even increase pleasantness for the principals in question, that is at least supposing they actually know what it is that they want. A hard "ask" I know.
Do you think so? It seems to me that they change with little to no warning, and so long as the business is willing to pay for the change, I can't see anything about them being objectively wrong.
Is the value just calling out the things that are most likely to change in a single place?
If anything, I find logically coherent software to be more pleasant (Rust) than something shitty (Python).
And if anything, commercial success seems to be inversely proportional to "pleasantness"
I am not against formal logic, in fact, I am probably more interested by it than most of my fellow programmers, but that's not my main focus of interest. If it was my passion, I would probably have gone for a maths PhD or something like that. No, I code to make the computer do cool stuff and formal analysis may be fun for some time but it quickly gets in the way.
On a more professional note, I code so that my company can make money and pay me, my company need users who pay to make money, therefore, I code to chase users. Proven software is expensive and very few users need that much, so we don't do it.
So if most programmers don't find it fun because they are more makers than scholars and it doesn't really help making money, then it is no surprise that it isn't done often.
I agree with the spirit of your comment. I want to add that the defining characteristic of becoming proficient at a technique is that it no longer gets in the way. Touch typing is a good example: when you totally lack proficiency hunt and peck is actually faster. In fact I’ve seen people get up to around 30-50 wpm that way. Having to constantly rehome and remember where the keys are and learn the muscle memory definitely “gets in the way” at first. I think you’ll find if you take the necessary hours that once you achieve proficiency doing things like constructing a nontrivial loop without using an invariant and variant will be considerably more and not less cumbersome.
That said, for exploratory programming, which a lot of professional work frankly is, I don’t find it particularly helpful to worry about proofs until I have a solid grasp on what it is I might want to prove.
He picked the metaphor. He could have picked trains instead. "Who drives a train around on rails? Do they guide you places? Yes."
Automated tests aren't all that useful to make sure that the code you just wrote does the right thing. People can and do use informal manual testing for that, plus careful crafting and review of the code.
Where automated tests really shine is in preventing your shiny new PR from accidentally messing up the feature you implemented a month ago.
Yes, tests can be wrong. They are still useful for the above, though.
Take the above, for example. If were to change the metaphor and say: "you know what's true about every fatal car accident where everyone was wearing a seatbelt? Everyone was wearing a seatbelt!" This is the _identical_ rhetorical argument that was made above, but when phrased this way it becomes obvious that it makes no argument.
And by the way, you don't necessarily want accidents to go to zero either. If we wanted that, that would be trivial to achieve: just ban driving. What we want to achieve is a particular trade-off between costs and benefits. In practice we behave as-if human life has a rather finite value, and trade off against it when making traffic decisions.
However, Rich Hickey's talk was the equivalent of "you know what's true about every fatal car accident where everyone was wearing a seatbelt? Everyone was wearing a seatbelt! [Laughs] Thus seatbelts suck."
-- Donald Knuth
That's quite the understatement.
> Unfortunately, if given the opportunity by a lax predicate, C-Reduce will write programs that have undefined behavior
I don't think this is true, in the introduction of [1]:
> Our reducers do this automatically and without introducing undefined behavior into the reduced test cases
[1] https://users.cs.utah.edu/~regehr/papers/pldi12-preprint.pdf