Given the popularity of TDD as modern cargo-cult "software correctness" practice, it's not clear to me why property-based testing (which can actually help improve correctness, even when most TDD effort could be replaced by a very simple type system) is only barely mentioned so far down in the article. Felt like a missed chance to provide some much needed guidance on these topics.
It'd be nice if TDD started to mean 'Type-Driven Development' in the world of software correctness. I believe it's a much better way of writing, such that a project leveraging the type system in that way would be of better quality than a test-driven development project.
This is actually how I approach software development generally. I write the types as the first test(s). Despite claims to the contrary, this makes prototyping and experimenting really convenient, and I can use my type checker/IDE as a test runner without setting up any project config. It’s just… limited.
That's what TDD seems to mean to Edwin Brady, whose book is "Type-Driven Development with Idris" [1].
Idris [2] is a Haskell-like language, but unlike Haskell it's strict and from the beginning was designed around a dependent type system. (Types and values exist on the same level, so that types can include values, be passed as arguments to functions, and be returned by functions.)
In the book Brady encourages you to create the skeleton of a function, then leverage the type system to help flesh it out.
> even when most TDD effort could be replaced by a very simple type system
I work daily in TypeScript, which has a notoriously (albeit adored by some, including me) complex type system, and I find this claim absolutely unbelievable. Not the claim itself, but the seriousness of saying it. I know sound type systems in ML-family languages are incredibly powerful, but they still only tell part of the story for even really basic problems. Types are a form of testing, of course. But if you’re writing your correctness check into a fib type signature, in any language, I think you’re probably gonna raise some eyebrows in review.
Most people write tests without applying TDD. TDD is a very inflexible process for writing tests, it might help people start writing tests but it is useless for those who already write tests.
Note: In some cases it makes sense to first write a failing test case, like when you found a bug you reproduce the bug in a test and then you fix it. But it doesn't make sense to write a green field project like that.
I’m not most people, I can only speak for myself. But my experience has been dramatically different. I was reluctant to adopt testing, and found test-first/red-green-refactor TDD totally alien. As I embraced testing at all, TDD became more interesting. As I tried it, just like with static typing, I found a tool I couldn’t imagine ever working without again.
I have to, because the world is imperfect. But greenfield is exactly where I find TDD shines. It’s untested code that I have to maintain that make TDD difficult, because untested code is often untestable and inscrutable.
Often even in those situations the very first thing I do, before I make a change, is test existing behavior as I understand it. Just so I have some sort of safety net changing a tiny thing which might have much larger ramifications I didn’t consider at that particular place in the code. Likewise, one of the first things I do entering a codebase in this condition is I start documenting it, with statically analyzable types. Again, testing first.
The only real exception is when there’s such a huge corpus of untested, hard to understand code that exploring the runtime is the most plausible way to get footing to get back to that approach.
I understand this isn’t how everyone feels. But I sincerely find it more valuable than trying to work in any other direction, and it’s only grown stronger the longer I’ve been working in software.
I find it makes sense if you can write the tests at a high enough level and the tooling to mock the "outside world" of your system is easy enough to use.
If you're doing TDD exclusively with unit tests I find it falls flat for pretty much everything except complex, logical code with no state and simple inputs and outputs.
Likewise I tried doing TDD on code which had complex, hard to mock interfaces to the outside world (e.g. interfacing with a horrible oracle system) and it didnt exactly become impossible but it definitely stopped being worthwhile.
> If you're doing TDD exclusively with unit tests I find it falls flat for pretty much everything except complex, logical code with no state and simple inputs and outputs.
This is absolutely true. And it’s not a coincidence I embraced TDD at the same time I was learning FP. And I continue to generally prefer both TDD and a FP style no matter what stack I’m working in.
Even simple type systems like in Java can help with correctness. For example if you have a list of "Person" but the code itself assumes it's a unique list of people you can convert that list to a Map<PersonId, Person>. Further if the map is assumed to never accept null values for either key or value you can capture that in some kind of "People" class that enforces invariant assumptions.
You're right that is does not prevent actual logic bugs but in practice, a lot of bugs are sometimes caused simply by bad inputs. With types you can make it so that logic never gets bad input eg (sqrt(NonNegativeDouble) instead of sqrt(double)) can potentially eliminate some error handling code.
I disagree strongly that types have nothing to do with correctness. Primitive types will only give you a limited utility, more complex type systems give you a lot more.
Obviously, bugs which exist at a highér level than whatever automated correctness system you employ can't be handled by it and need something else.
I'm upvoting you, because while I don't agree with you, downvotes shouldn't be used to express disagreement.
I agree that types can help with sanity of data flowing in and out, but how do you check the correctness of program with types?
Example: your function is doing some complex calculation, while the inputs types can be strongly checked and output types can be checked, but the logic has to be tested by writing unit tests right?
The original comment which i replied to suggests that we can get rid of TDD only if we employ using type systems, which i feel is over exaggeration of the benefits of the types
Yep, nothing gives you complete assurance of correctness. Even formal methods can have bugs in the specification.
It's good for the compiler to provide correctness guarantees where it can, but tests find different bugs. I think they are useful things to have.
Having said that, I once did an analysis of tests vs bugs in a fairly large code base. There was almost no correlation between number of tests and number of bugs.
Most bugs caught in the wild were actually failures of the developer to fully understand the spec. We had tests that enforced the incorrect understanding!
> most TDD effort could be replaced by a very simple type system
I'm not convinced that's true. When writing Python, even before tools like mypy, most of my tests weren't assertions about types. They involved types implicitly, and so functioned as a form of type checking. But most of my tests were about invariants and specific oracles
For example, I don't need to check that a result is a `str` if I'm checking that it starts with "my-prefix".
I'd be much more inclined to say that a simple contract system could replace most unit tests.
The big difference is the amount of inputs you have to test for, dynamic languages can fail in infinitely more ways.
In a compile time type checked language you know what types can be passed to the function so the amount of possible execution paths is much lower. and in many cases the type checking itself is enough for you to be confident that the code works. In dynamic languages you always need a test that executed the code as even small things like typos will cause the code to fail at runtime.
I tend to find that "wrong type" accounts for a vanishingly small % of production bugs in average python programs.
The only exceptions I experienced this on were on A) projects that had zero tests and B) projects that insisted on passing around dicts and primitives rather than classes.
If the project developed a mimimal level of testing that one might tentatively argue that you'd want anyway to validate behavior and made half an attempt to use OO this class of bug seemed to dry up pretty quickly.
I've also seen Java developers switch to python and write entirely untested code and then get frustrated that they got type errors at runtime that the Java compiler used to catch for them. I wouldnt exactly say I felt sympathetic to their plight.
I find that people have very different understandings of what "wrong type" means.
If you restrict yourself to places where python or js actually mention type in the error messages, that misses a whole lot of things that basic use of a simple type system would catch, much less skilled use of a sophisticated type system.
There's an example I give - admittedly tangential given that it does not replace (and could not be replaced by) unit tests, but hopefully giving some insight into the range of what's possible: I once used C's type system to catch "you called this function from the wrong thread" at compile time, converting subtle runtime failures or meaningful runtime overhead into "you can't call this here, dummy" before running anything. This was hugely helpful as requirements evolved and I found myself moving large pieces of functionality between threads.
I don't think this clearly resolves the broader discussion; static type checking is a tool and its applicability may well depend on the problems at hand, the language in question, and the developers involved; I think how it should be applied certainly depends on these things. But I think it is too often dismissed based on an overly narrow understanding of what a "type error" can be.
I use asserts in python in a similar manner to the way you used types in C. Combined with tests it's a highly flexible way of "locking down" behaviors that should be impossible.
> most of my tests weren't assertions about types. They involved types implicitly, and so functioned as a form of type checking. But most of my tests were about invariants and specific oracles
While it's true that most type systems are not capable of completely replacing tests (and for those where they might be possible, you might not want to), it's also important to point out that the real gains from types aren't from "oh make sure that this input is actually an integer and not a boolean." If you have the following three features, which a lot of type systems have, you can get a ton of mileage far beyond simple "wrong shape" errors.
1. Exhaustivity checking of different type variants (e.g. things like `type NonBooleanLogic = True or False or Unknown` whether that's implemented through sealed subclassing or sum types) when you write logic that switches against different variants (i.e.
switch(myNonBooleanLogicResult) on {
True -> // Do something
False -> // Do something
// Typechecker errors out and tells you that you've failed to cover the Unknown case
}
).
2. Ability to cheaply make new types
3. Ability to make certain type constructors and functions private
For example how do I ensure that all data passing through our codebase that makes it into our database is sanitized? Make a `Sanitized` type with a private constructor which can only be constructed in the function that actually performs sanitization. Then make the input type to the function that writes to the database `Sanitized` and hide the non-sanitized input function as a private function that can't be accessed anywhere else. Tada now you have very high confidence that all data going into your database is sanitized, no matter how many code paths in your codebase you have that ultimately write to the database. By making the constructor private, you've ensured that all those code paths must've called the sanitization function somewhere (and if you make `Sanitized` immutable you've also ensured that it cannot be tampered with after being sanitized).
Likewise if I had a bunch of code that consumed and produced `NonBooleanLogic`s and I wanted to add a new value to `NonBooleanLogic` such as `NeitherTrueNorFalse` , then I don't need to go up to various coworker and ask about all the places in various modules that I should change to make sure that they all process this new `NeitherTrueNorFalse` value correctly. I just add it to `NonBooleanLogic` and the typechecker plays the role of my coworkers, going around and pointing out every part in the codebase that requires my attention.
There's a bunch of these simple tricks that seem inconsequential on their own, but taken together greatly increase confidence when refactoring code or adding new features to a preexisting codebase that you've done everything correctly, more so than what "oh just make sure this integer isn't a boolean" would seem to entail.
Contracts are typically for higher order behaviors than unit tests target. They're for the component/service functional granularity.
Contract testing is great, though. And given that the contracts are about behaviors, they're a great candidate for BDD. (But please hold the Cucumber!)
I know when I don't floss my mouth tastes and smells terrible and that I quickly develop tartar, I don't need a peer reviewed study to know that what I'm tasting is bacteria multiplying in my mouth.
I think the term for your way of thinking is scientism? If you can't even make conclusions for yourself based on simple experimentation or observation and need to rely on studies for everything you are going to live a terrible life.
Oh, and the OP doesn't even have research that flossing doesn't work. He just has people dropping the flossing recommendation because of lack of research. OP probably uses this stupidity to justify being completely unhygienic.
My dad's dentist had a picture on the wall that said "You only have to floss between the teeth you want to keep".
When I floss after not doing so for a long time I get a whiff and taste of decaying matter. It is disgusting. Good enough evidence for me, though I still don't floss often :(
I don't buy that for a second. Every dentist I've ever seen not only tells me to do so, but can tell immediately just by looking whether I'm lying or not. I wasn't a great flosser in my teens, and do so religiously now, so have experienced both sides.
Secondly, have you ever -smelled- the result of flossing after even missing one day?
Anecdotes aside, I just Googled to have a reference, and it seems scientific enough and in favor of flossing -
"An analysis of 12 well-controlled studies found that flossing plus toothbrushing reduced mild gum disease, or gingivitis, significantly better than toothbrushing alone."
I don’t believe it either. I had gingivitis before flossing, now never. I also had cavities appearing between my teeth, but not anymore.
I read these articles too a few years ago, and I wondered if most of the people were just bad at flossing or something. But yea it just doesn’t quite align with my personal experience, or the experience of my dentist. I know firsthand that scientists can and do often get it wrong. I think this may be one example of that.
The author posits that people won't do inconvenient things whose benefit massively outweighs the cost.
It's certainly true that making anything easier to use helps adoption of whatever the thing is.
I'm less convinced by his arguments that different communities of correctness think the others don't care about correctness. They may believe theirs is better, more useful or easier to adopt, but I don't think I've heard TDD people say formal methods people don't care about correctness!
As someone who's been developing professionally for over a decade and a half now, I think the author misses one *major* critical point.
Regardless of whether or not a programmer cares about correctness, most programmers don't work in academia on toy projects. They work in the real world - with 15 year old codebases, tons of dependencies, integrations with other systems, deadlines and commitments, budget constraints, and a team who were all hired to work on that type of code, not some other type of code with different processes and tools.
No matter how much a programmer might prefer to have strong compiler-time type checks, or full test coverage, or design-by-contract, or a codebase written with literate programming, or whatever.
They can't just go off and spend several years rewriting the entire system and all its dependencies, using different languages, tools, methods, etc., to be 'better'. Especially not when it already mostly works and the company already has processes in place to deal with bugs.
They have to work within, and gradually evolve, the existing systems and processes. And do so in a way that's compatible with all the other stuff it has to interact with (dependencies, customer system integrations, etc.) without disrupting service. While still delivering new features and fixes.
And that is a massively more difficult problem than simply using whatever your favored technique is to write 'correct' code from the start on a brand new and self-contained toy project.
It's not difficult to use any of those tools or techniques. But it's quite difficult indeed to use them in many/most professional projects.
The main thing that's needed is good easy ways to gradually evolve a system to use them, especially when it's a partially-controlled system. Progress is being made, but at a glacial pace. Saying "programmers don't care" is mostly pointless and wrong, programmers hate dealing with bugs. They'd be happy to have the system prevent a great many of them.
36 comments
[ 0.16 ms ] story [ 94.9 ms ] threadIdris [2] is a Haskell-like language, but unlike Haskell it's strict and from the beginning was designed around a dependent type system. (Types and values exist on the same level, so that types can include values, be passed as arguments to functions, and be returned by functions.)
In the book Brady encourages you to create the skeleton of a function, then leverage the type system to help flesh it out.
[1] https://www.manning.com/books/type-driven-development-with-i...
[2] https://www.idris-lang.org/index.html
I work daily in TypeScript, which has a notoriously (albeit adored by some, including me) complex type system, and I find this claim absolutely unbelievable. Not the claim itself, but the seriousness of saying it. I know sound type systems in ML-family languages are incredibly powerful, but they still only tell part of the story for even really basic problems. Types are a form of testing, of course. But if you’re writing your correctness check into a fib type signature, in any language, I think you’re probably gonna raise some eyebrows in review.
Note: In some cases it makes sense to first write a failing test case, like when you found a bug you reproduce the bug in a test and then you fix it. But it doesn't make sense to write a green field project like that.
I have to, because the world is imperfect. But greenfield is exactly where I find TDD shines. It’s untested code that I have to maintain that make TDD difficult, because untested code is often untestable and inscrutable.
Often even in those situations the very first thing I do, before I make a change, is test existing behavior as I understand it. Just so I have some sort of safety net changing a tiny thing which might have much larger ramifications I didn’t consider at that particular place in the code. Likewise, one of the first things I do entering a codebase in this condition is I start documenting it, with statically analyzable types. Again, testing first.
The only real exception is when there’s such a huge corpus of untested, hard to understand code that exploring the runtime is the most plausible way to get footing to get back to that approach.
I understand this isn’t how everyone feels. But I sincerely find it more valuable than trying to work in any other direction, and it’s only grown stronger the longer I’ve been working in software.
If you're doing TDD exclusively with unit tests I find it falls flat for pretty much everything except complex, logical code with no state and simple inputs and outputs.
Likewise I tried doing TDD on code which had complex, hard to mock interfaces to the outside world (e.g. interfacing with a horrible oracle system) and it didnt exactly become impossible but it definitely stopped being worthwhile.
This is absolutely true. And it’s not a coincidence I embraced TDD at the same time I was learning FP. And I continue to generally prefer both TDD and a FP style no matter what stack I’m working in.
Writing tests before you implement is like flossing before you eat, it creates a lot of behaviour that are correlated with good results.
But who's going to verify the logic if not tests, types won't be of much use here.
You're right that is does not prevent actual logic bugs but in practice, a lot of bugs are sometimes caused simply by bad inputs. With types you can make it so that logic never gets bad input eg (sqrt(NonNegativeDouble) instead of sqrt(double)) can potentially eliminate some error handling code.
Obviously, bugs which exist at a highér level than whatever automated correctness system you employ can't be handled by it and need something else.
I'm upvoting you, because while I don't agree with you, downvotes shouldn't be used to express disagreement.
Example: your function is doing some complex calculation, while the inputs types can be strongly checked and output types can be checked, but the logic has to be tested by writing unit tests right?
The original comment which i replied to suggests that we can get rid of TDD only if we employ using type systems, which i feel is over exaggeration of the benefits of the types
ps: Thanks for the upvote :)
It's good for the compiler to provide correctness guarantees where it can, but tests find different bugs. I think they are useful things to have.
Having said that, I once did an analysis of tests vs bugs in a fairly large code base. There was almost no correlation between number of tests and number of bugs.
Most bugs caught in the wild were actually failures of the developer to fully understand the spec. We had tests that enforced the incorrect understanding!
I'm not convinced that's true. When writing Python, even before tools like mypy, most of my tests weren't assertions about types. They involved types implicitly, and so functioned as a form of type checking. But most of my tests were about invariants and specific oracles
For example, I don't need to check that a result is a `str` if I'm checking that it starts with "my-prefix".
I'd be much more inclined to say that a simple contract system could replace most unit tests.
In a compile time type checked language you know what types can be passed to the function so the amount of possible execution paths is much lower. and in many cases the type checking itself is enough for you to be confident that the code works. In dynamic languages you always need a test that executed the code as even small things like typos will cause the code to fail at runtime.
The only exceptions I experienced this on were on A) projects that had zero tests and B) projects that insisted on passing around dicts and primitives rather than classes.
If the project developed a mimimal level of testing that one might tentatively argue that you'd want anyway to validate behavior and made half an attempt to use OO this class of bug seemed to dry up pretty quickly.
I've also seen Java developers switch to python and write entirely untested code and then get frustrated that they got type errors at runtime that the Java compiler used to catch for them. I wouldnt exactly say I felt sympathetic to their plight.
I find that people have very different understandings of what "wrong type" means.
If you restrict yourself to places where python or js actually mention type in the error messages, that misses a whole lot of things that basic use of a simple type system would catch, much less skilled use of a sophisticated type system.
There's an example I give - admittedly tangential given that it does not replace (and could not be replaced by) unit tests, but hopefully giving some insight into the range of what's possible: I once used C's type system to catch "you called this function from the wrong thread" at compile time, converting subtle runtime failures or meaningful runtime overhead into "you can't call this here, dummy" before running anything. This was hugely helpful as requirements evolved and I found myself moving large pieces of functionality between threads.
I don't think this clearly resolves the broader discussion; static type checking is a tool and its applicability may well depend on the problems at hand, the language in question, and the developers involved; I think how it should be applied certainly depends on these things. But I think it is too often dismissed based on an overly narrow understanding of what a "type error" can be.
While it's true that most type systems are not capable of completely replacing tests (and for those where they might be possible, you might not want to), it's also important to point out that the real gains from types aren't from "oh make sure that this input is actually an integer and not a boolean." If you have the following three features, which a lot of type systems have, you can get a ton of mileage far beyond simple "wrong shape" errors.
1. Exhaustivity checking of different type variants (e.g. things like `type NonBooleanLogic = True or False or Unknown` whether that's implemented through sealed subclassing or sum types) when you write logic that switches against different variants (i.e.
).2. Ability to cheaply make new types
3. Ability to make certain type constructors and functions private
For example how do I ensure that all data passing through our codebase that makes it into our database is sanitized? Make a `Sanitized` type with a private constructor which can only be constructed in the function that actually performs sanitization. Then make the input type to the function that writes to the database `Sanitized` and hide the non-sanitized input function as a private function that can't be accessed anywhere else. Tada now you have very high confidence that all data going into your database is sanitized, no matter how many code paths in your codebase you have that ultimately write to the database. By making the constructor private, you've ensured that all those code paths must've called the sanitization function somewhere (and if you make `Sanitized` immutable you've also ensured that it cannot be tampered with after being sanitized).
Likewise if I had a bunch of code that consumed and produced `NonBooleanLogic`s and I wanted to add a new value to `NonBooleanLogic` such as `NeitherTrueNorFalse` , then I don't need to go up to various coworker and ask about all the places in various modules that I should change to make sure that they all process this new `NeitherTrueNorFalse` value correctly. I just add it to `NonBooleanLogic` and the typechecker plays the role of my coworkers, going around and pointing out every part in the codebase that requires my attention.
There's a bunch of these simple tricks that seem inconsequential on their own, but taken together greatly increase confidence when refactoring code or adding new features to a preexisting codebase that you've done everything correctly, more so than what "oh just make sure this integer isn't a boolean" would seem to entail.
Contract testing is great, though. And given that the contracts are about behaviors, they're a great candidate for BDD. (But please hold the Cucumber!)
https://news.ycombinator.com/item?id=12216127 6 years ago Federal health expert drop flossing from health guideline
https://news.ycombinator.com/item?id=27524152 8 months ago The AP asked the government for proof that flossing works. The answer: ¯\_(ツ)_/¯
I think the term for your way of thinking is scientism? If you can't even make conclusions for yourself based on simple experimentation or observation and need to rely on studies for everything you are going to live a terrible life.
When I floss after not doing so for a long time I get a whiff and taste of decaying matter. It is disgusting. Good enough evidence for me, though I still don't floss often :(
Secondly, have you ever -smelled- the result of flossing after even missing one day?
Anecdotes aside, I just Googled to have a reference, and it seems scientific enough and in favor of flossing -
https://newsinhealth.nih.gov/2016/11/dont-toss-floss#:~:text....
"An analysis of 12 well-controlled studies found that flossing plus toothbrushing reduced mild gum disease, or gingivitis, significantly better than toothbrushing alone."
I read these articles too a few years ago, and I wondered if most of the people were just bad at flossing or something. But yea it just doesn’t quite align with my personal experience, or the experience of my dentist. I know firsthand that scientists can and do often get it wrong. I think this may be one example of that.
It's certainly true that making anything easier to use helps adoption of whatever the thing is.
I'm less convinced by his arguments that different communities of correctness think the others don't care about correctness. They may believe theirs is better, more useful or easier to adopt, but I don't think I've heard TDD people say formal methods people don't care about correctness!
Regardless of whether or not a programmer cares about correctness, most programmers don't work in academia on toy projects. They work in the real world - with 15 year old codebases, tons of dependencies, integrations with other systems, deadlines and commitments, budget constraints, and a team who were all hired to work on that type of code, not some other type of code with different processes and tools.
No matter how much a programmer might prefer to have strong compiler-time type checks, or full test coverage, or design-by-contract, or a codebase written with literate programming, or whatever.
They can't just go off and spend several years rewriting the entire system and all its dependencies, using different languages, tools, methods, etc., to be 'better'. Especially not when it already mostly works and the company already has processes in place to deal with bugs.
They have to work within, and gradually evolve, the existing systems and processes. And do so in a way that's compatible with all the other stuff it has to interact with (dependencies, customer system integrations, etc.) without disrupting service. While still delivering new features and fixes.
And that is a massively more difficult problem than simply using whatever your favored technique is to write 'correct' code from the start on a brand new and self-contained toy project.
It's not difficult to use any of those tools or techniques. But it's quite difficult indeed to use them in many/most professional projects.
The main thing that's needed is good easy ways to gradually evolve a system to use them, especially when it's a partially-controlled system. Progress is being made, but at a glacial pace. Saying "programmers don't care" is mostly pointless and wrong, programmers hate dealing with bugs. They'd be happy to have the system prevent a great many of them.