5 ms·

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 t

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.

User23 3y ago
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.
- Kamq 3y ago
  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 3y ago
    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.
mrkeen 3y ago
> 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."
- naasking 3y ago
  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.
- astrange 3y ago
  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.
  - eru 3y ago
    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.
- taeric 3y ago
  Of course, that is also a useful metaphor here. They do guide you places, and prevent you from making any slight changes to your route. And make it so one stuck train blocks the line.
3193528104 3y ago
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.
- tacitusarc 3y ago
  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.
  - justinjlynn 3y ago
    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.
  - eru 3y ago
    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.
    - deleted 3y ago
      [deleted]

User23 3y ago

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.

Kamq 3y ago
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 3y ago
  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.

mrkeen 3y ago

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

naasking 3y ago
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.
astrange 3y ago
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.
- eru 3y ago
  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.
taeric 3y ago
Of course, that is also a useful metaphor here. They do guide you places, and prevent you from making any slight changes to your route. And make it so one stuck train blocks the line.

3193528104 3y ago

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.

tacitusarc 3y ago
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.
- justinjlynn 3y ago
  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.
- eru 3y ago
  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.
  - deleted 3y ago
    [deleted]