[HN Gopher] Testing a Formally Verified Compiler
___________________________________________________________________
Testing a Formally Verified Compiler
Author : luu
Score : 93 points
Date : 2023-05-21 05:33 UTC (17 hours ago)
(HTM) web link (hal.science)
(TXT) w3m dump (hal.science)
| mafribe wrote:
| 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]_"
| DonaldPShimoda wrote:
| An excellent clarification to make.
|
| "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).
| crdrost wrote:
| 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.
| mrkeen wrote:
| > Right. I think we're in this world that I like to call guard-
| rail programming.
|
| He picked the metaphor. He could have picked trains instead.
| "Who drives a train around on rails? Do they guide you places?
| Yes."
| 3193528104 wrote:
| 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.
| User23 wrote:
| 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.
| GuB-42 wrote:
| 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.
| Kamq wrote:
| 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.
| User23 wrote:
| 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.
| Kamq wrote:
| > 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?
| fnord77 wrote:
| 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"
| grumpyprole wrote:
| 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.
| thanatos519 wrote:
| Beware of bugs in the above code; I have only proved it correct,
| not tried it.
|
| -- Donald Knuth
| red75prime wrote:
| I'd be content if the compiler was also written by Knuth and
| the processor was designed by Knuth and physical laws was
| created by Knuth.
___________________________________________________________________
(page generated 2023-05-21 23:00 UTC)