31–34 of 34 posts
> 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
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…
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 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."
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.
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 "y…