Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Testing a Formally Verified Compiler

hal.science

Post reply on HN
Print view View original

11–20 of 34 posts

Re: Testing a Formally Verified Compiler

#11

Post by 3193528104 »

crdrost wrote: post #4

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 l…

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.

Re: Testing a Formally Verified Compiler

#12

Post by User23 »

Kamq wrote: post #8
User23 wrote: post #6

Earlier quoted context omitted.

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 an…

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…

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.

Re: Testing a Formally Verified Compiler

#14

Post by Kamq »

User23 wrote: post #12
Kamq wrote: post #8

Earlier quoted context omitted.

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…

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"…

> 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?

Re: Testing a Formally Verified Compiler

#15

Post by GuB-42 »

User23 wrote: post #6
crdrost wrote: post #4

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 l…

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 an…

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.

Re: Testing a Formally Verified Compiler

#16

Post by naasking »

mrkeen wrote: post #7
crdrost wrote: post #4

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 l…

> 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."

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.

Re: Testing a Formally Verified Compiler

#17

Post by User23 »

Kamq wrote: post #14
User23 wrote: post #12

Earlier quoted context omitted.

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"…

> 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 j…

There’s certainly value there, but to give Mr. Hickey his due informal reasoning has been, in my experience, mostly adequate for properly separating those kinds of concerns. I would like to think we can do even better though, and so far as I can tell those sorts of informal methods have been refined to essentially peak performance.

I expect there is opportunity for business friendly consequences like proving that no edge case exists that can drain your wallet.

Re: Testing a Formally Verified Compiler

#18

Post by astrange »

mrkeen wrote: post #7
crdrost wrote: post #4

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 l…

> 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."

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.

Re: Testing a Formally Verified Compiler

#19

Post by astrange »

DonaldPShimoda wrote: post #3
mafribe wrote: post #2

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,…

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. Withi…

> "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).

Re: Testing a Formally Verified Compiler

#20

Post by naasking »

Kamq wrote: post #14
User23 wrote: post #12

Earlier quoted context omitted.

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"…

> 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 j…

Formally specifying requirements earlier often reveals inconsistencies and limitations that otherwise only users will reveal in acceptance testing or after deployment.
Post reply on HN