Testing a Formally Verified Compiler

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.

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.

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

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.

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