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

21–30 of 34 posts

Re: Testing a Formally Verified Compiler

#21

Post by tacitusarc »

3193528104 wrote: post #11
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 k…

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.

Re: Testing a Formally Verified Compiler

#22

Post by justinjlynn »

tacitusarc wrote: post #21
3193528104 wrote: post #11

Earlier quoted context omitted.

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

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.

Re: Testing a Formally Verified Compiler

#23

Post by taeric »

red75prime wrote: post #13
thanatos519 wrote: post #5

Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald Knuth

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.

Oddly, he wouldn't. He very much appreciates exploring the work of others. Such that large portions of his writing is historical in nature.

Re: Testing a Formally Verified Compiler

#24

Post by eru »

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

That's quite the understatement.

Re: Testing a Formally Verified Compiler

#25

Post by eru »

tacitusarc wrote: post #21
3193528104 wrote: post #11

Earlier quoted context omitted.

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

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.

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.

Re: Testing a Formally Verified Compiler

#26

Post by eru »

astrange wrote: post #18
mrkeen wrote: post #7

Earlier quoted context omitted.

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

To give a practical perspective:

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.

Re: Testing a Formally Verified Compiler

#27

Post by 3193528104 »

tacitusarc wrote: post #21
3193528104 wrote: post #11

Earlier quoted context omitted.

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

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.

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

Re: Testing a Formally Verified Compiler

#28

Post by User23 »

GuB-42 wrote: post #15
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…

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

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

Re: Testing a Formally Verified Compiler

#29

Post by wtroughton »

astrange wrote: post #19
DonaldPShimoda wrote: post #3

Earlier quoted context omitted.

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

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?

Re: Testing a Formally Verified Compiler

#30

Post by [deleted] »

eru wrote: post #25
tacitusarc wrote: post #21

Earlier quoted context omitted.

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.

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…

[deleted]
Post reply on HN