3 ms·

Correctness advocates like the author tend to take the concept of "correct" for granted. 99% of software projects don't have a reliable definition of "correct"

Correctness advocates like the author tend to take the concept of "correct" for granted. 99% of software projects don't have a reliable definition of "correct". They don't have a watertight ontology that you can infer types from. Requirements continuously change. Your "Whys" quickly end with "because so-and-so said so", and will change tomorrow. "What if?" Driven Development presumes that there is a finite and known set of states that you can design around. Most software development (outside of extremely well-studied domains, like financial exchanges and aerospace) occurs in the absence of well-defined specifications. That's the fundamental reason why correctness-oriented paradigms and languages aren't popular and never will be. And that's okay.

goostavos 3y ago
I'll give a slightly different take. I work on large financial systems at $MegaCorp. Even though requirements change all the time (often because "the government said so"), are ephemeral at best, and frequently contradictory due crossing entire teams, orgs, and charters.... Stealing every possible tool that can move the needle towards "correctness" has been crazy valuable in my experience. I've gotten on board the TLA+ train. Just the act of formally specifying what you do know makes everything you don't painfully obvious. Formal models also make dealing with that constant change easier, because The Rules live in one concrete place, in a formal modeling language, and free from the ambiguities that requirements expressed in English prose are subject to. It's not a perfect solution, but it can help cut through the noise.
- pphysch 3y ago
  More power to you in specifying your processes. A potential issue here is that your bosses and other stakeholders aren't part of the specification meta-process. Can you talk TLA+ with your boss? What about your boss's boss? Do they even care? A bad specification is worse than no specification; this was one of the lessons of OOP-mania (a rigid ontology works great, until it doesn't, and then it's a disaster). An ostensibly correct "specification" inferred by a lone engineer could become Wrong tomorrow after stakeholder input. That's why I would recommend against these sort of correctness-oriented paradigms unless there is widespread buy-in and understanding from your stakeholders, company culture, etc. Of course there is merit to using tools like TLA+ to model distributed systems and assist development, but that shouldn't be conflated with having a well-defined specification from the get-go.
crocsocks 3y ago
Yep, tough to type business logic.
hbrn 3y ago
Certain teams do suffer from incorrectness they produce, and I think obsession with correctness can be beneficial for them. But it's a painkiller, not a cure. Once you build a good team, the source of incorrectness shifts to the vagueness of the requirements and domain complexity. And indeed, attempting to solve it (be it with types or with tests) is pointless. In essence, if your team finds a lot of benefits in types, you have a mediocre team. And mediocrity is almost unavoidable at scale, that's why big companies heavily invest into those correctness procedures (unit tests, types, various forms of bureaucracy, etc).
- hinkley 3y ago
  When everything is special, nothing is special. Pick some battles, fight them well, let everything else you do be as boring as you can possibly make it.
jacobyoder 3y ago
> Your "Whys" quickly end with "because so-and-so said so", and will change tomorrow. The "5 whys" always seemed to stop just short of formally identifying the root cause of conflicting management techniques, inexperienced decision makers, poor planning and people not understanding the technology they were making decisions and deadlines around. I saw this first hand a couple years back, except... we always seemed to stop one step short of the "so and so said so" because... "we don't want to blame people". So often it would stop at me, instead of going one more level up beyond me to the people who gave me impossible/contradictory things to do. So, to get past the "no blame" thing, I got "we're not 'blaming' you, but perhaps you need more training on X" and that sort of thing. I've been doing this professionally longer than most of the rest of the team have been adults (or in some cases, alive)... no, I don't need more training on X. The system didn't fail because I hit a problem with X. The system failed because 3 people set too many deadlines concurrently, and when it was pointed out to everyone (individually, then in a group setting), no one would budge and I get told "just make it happen". Laws of physics, etc. But... let's make sure we don't "blame" people! Just... it's OK if we blame you, we just won't call it 'blame'. We're just "identifying".

goostavos 3y ago

I'll give a slightly different take. I work on large financial systems at $MegaCorp. Even though requirements change all the time (often because "the government said so"), are ephemeral at best, and frequently contradictory due crossing entire teams, orgs, and charters.... Stealing every possible tool that can move the needle towards "correctness" has been crazy valuable in my experience. I've gotten on board the TLA+ train. Just the act of formally specifying what you do know makes everything you don't painfully obvious. Formal models also make dealing with that constant change easier, because The Rules live in one concrete place, in a formal modeling language, and free from the ambiguities that requirements expressed in English prose are subject to. It's not a perfect solution, but it can help cut through the noise.

pphysch 3y ago
More power to you in specifying your processes. A potential issue here is that your bosses and other stakeholders aren't part of the specification meta-process. Can you talk TLA+ with your boss? What about your boss's boss? Do they even care? A bad specification is worse than no specification; this was one of the lessons of OOP-mania (a rigid ontology works great, until it doesn't, and then it's a disaster). An ostensibly correct "specification" inferred by a lone engineer could become Wrong tomorrow after stakeholder input. That's why I would recommend against these sort of correctness-oriented paradigms unless there is widespread buy-in and understanding from your stakeholders, company culture, etc. Of course there is merit to using tools like TLA+ to model distributed systems and assist development, but that shouldn't be conflated with having a well-defined specification from the get-go.

crocsocks 3y ago

Yep, tough to type business logic.

hbrn 3y ago

Certain teams do suffer from incorrectness they produce, and I think obsession with correctness can be beneficial for them. But it's a painkiller, not a cure. Once you build a good team, the source of incorrectness shifts to the vagueness of the requirements and domain complexity. And indeed, attempting to solve it (be it with types or with tests) is pointless. In essence, if your team finds a lot of benefits in types, you have a mediocre team. And mediocrity is almost unavoidable at scale, that's why big companies heavily invest into those correctness procedures (unit tests, types, various forms of bureaucracy, etc).

hinkley 3y ago
When everything is special, nothing is special. Pick some battles, fight them well, let everything else you do be as boring as you can possibly make it.

jacobyoder 3y ago

> Your "Whys" quickly end with "because so-and-so said so", and will change tomorrow. The "5 whys" always seemed to stop just short of formally identifying the root cause of conflicting management techniques, inexperienced decision makers, poor planning and people not understanding the technology they were making decisions and deadlines around. I saw this first hand a couple years back, except... we always seemed to stop one step short of the "so and so said so" because... "we don't want to blame people". So often it would stop at me, instead of going one more level up beyond me to the people who gave me impossible/contradictory things to do. So, to get past the "no blame" thing, I got "we're not 'blaming' you, but perhaps you need more training on X" and that sort of thing. I've been doing this professionally longer than most of the rest of the team have been adults (or in some cases, alive)... no, I don't need more training on X. The system didn't fail because I hit a problem with X. The system failed because 3 people set too many deadlines concurrently, and when it was pointed out to everyone (individually, then in a group setting), no one would budge and I get told "just make it happen". Laws of physics, etc. But... let's make sure we don't "blame" people! Just... it's OK if we blame you, we just won't call it 'blame'. We're just "identifying".