4 ms·

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

by 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.
  - Kamq 3y ago
    > 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?
    - User23 3y ago
      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.
    - naasking 3y ago
      Formally specifying requirements earlier often reveals inconsistencies and limitations that otherwise only users will reveal in acceptance testing or after deployment.
fnord77 3y ago
This generalization has no merit. There's a very wide range of American software, from the formally verified Rust programming language to some Javascript shitlibs. Stanford and Berkeley are home to some very famous formalization efforts. If anything, I find logically coherent software to be more pleasant (Rust) than something shitty (Python). And if anything, commercial success seems to be inversely proportional to "pleasantness"
grumpyprole 3y ago
Americans also mostly don't study programming language theory (PLT) (unless they are lucky enough to attend e.g. Carnegie Mellon). A lot of the focus is on algorithms - which is a great shame. The majority of programmers will be consuming/creating APIs and abstractions, not implementing algorithms. PLT would be much more helpful here.
GuB-42 3y ago
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.
- User23 3y ago
  > 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.

by User23 3y ago

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.
- Kamq 3y ago
  > 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?
  - User23 3y ago
    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.
  - naasking 3y ago
    Formally specifying requirements earlier often reveals inconsistencies and limitations that otherwise only users will reveal in acceptance testing or after deployment.

fnord77 3y ago

This generalization has no merit. There's a very wide range of American software, from the formally verified Rust programming language to some Javascript shitlibs. Stanford and Berkeley are home to some very famous formalization efforts. If anything, I find logically coherent software to be more pleasant (Rust) than something shitty (Python). And if anything, commercial success seems to be inversely proportional to "pleasantness"

grumpyprole 3y ago

Americans also mostly don't study programming language theory (PLT) (unless they are lucky enough to attend e.g. Carnegie Mellon). A lot of the focus is on algorithms - which is a great shame. The majority of programmers will be consuming/creating APIs and abstractions, not implementing algorithms. PLT would be much more helpful here.

GuB-42 3y ago

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.

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