6 ms·

Software correctness is a lot like flossing (2020)

40 points by BerislavLopac 5y ago

stillbourne 5y ago
So it prevents code smells and code rot?
zozbot234 5y ago
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.
- exdsq 5y ago
  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.
  - eyelidlessness 5y ago
    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.
  - rotifer 5y ago
    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. [1] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i... [2] https://www.idris-lang.org/index.html https://www.idris-lang.org/index.html
- eyelidlessness 5y ago
  > 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.
  - Jensson 5y ago
    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.
    - eyelidlessness 5y ago
      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.
- Jensson 5y ago
  TDD is a good example of Godwin's Law, it is optimized to produce quantity of tests. Writing tests before you implement is like flossing before you eat, it creates a lot of behaviour that are correlated with good results.
- gvpmahesh 5y ago
  Types have nothing to do with correctness. The maximum you can be assured of you will be getting a integer, instead of string. But who's going to verify the logic if not tests, types won't be of much use here.
  - foo_barrio 5y ago
    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.
  - MattPalmer1086 5y ago
    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.
    - gvpmahesh 5y ago
      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 ps: Thanks for the upvote :)
- moeris 5y ago
  > 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.
  - Jensson 5y ago
    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.
    - pydry 5y ago
      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.
      - zppln 5y ago
        This is pretty much my experience as well, including the part about Java programmers.
birdyrooster 5y ago
Wait, hygiene in one context is similar to hygiene in a different context? What?? This revelation is worthy of follow on conversation.
deleted 5y ago
[deleted]
boogies 5y ago
There’s no strong scientific evidence in favor of flossing. https://news.ycombinator.com/item?id=12216127 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 https://news.ycombinator.com/item?id=27524152 8 months ago The AP asked the government for proof that flossing works. The answer: ¯\_(ツ)_/¯
- friedman23 5y ago
  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.
  - darkerside 5y ago
    Science is however great for combatting truthiness. Some things feel so true that the only way to change is to prove it with science.
    - friedman23 5y ago
      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.
    - deleted 5y ago
      [deleted]
  - 83457 5y ago
    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 :(
MattPalmer1086 5y ago
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!
Falkon1313 5y ago
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.

40 points by BerislavLopac 5y ago

So it prevents code smells and code rot?

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.

exdsq 5y ago
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.
- eyelidlessness 5y ago
  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.
- rotifer 5y ago
  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. [1] https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i... [2] https://www.idris-lang.org/index.html https://www.idris-lang.org/index.html
eyelidlessness 5y ago
> 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.
- Jensson 5y ago
  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.
  - eyelidlessness 5y ago
    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.
Jensson 5y ago
TDD is a good example of Godwin's Law, it is optimized to produce quantity of tests. Writing tests before you implement is like flossing before you eat, it creates a lot of behaviour that are correlated with good results.
gvpmahesh 5y ago
Types have nothing to do with correctness. The maximum you can be assured of you will be getting a integer, instead of string. But who's going to verify the logic if not tests, types won't be of much use here.
- foo_barrio 5y ago
  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.
- MattPalmer1086 5y ago
  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.
  - gvpmahesh 5y ago
    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 ps: Thanks for the upvote :)
moeris 5y ago
> 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.
- Jensson 5y ago
  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.
  - pydry 5y ago
    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.
    - zppln 5y ago
      This is pretty much my experience as well, including the part about Java programmers.

birdyrooster 5y ago

Wait, hygiene in one context is similar to hygiene in a different context? What?? This revelation is worthy of follow on conversation.

deleted 5y ago

[deleted]

boogies 5y ago

There’s no strong scientific evidence in favor of flossing. https://news.ycombinator.com/item?id=12216127 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 https://news.ycombinator.com/item?id=27524152 8 months ago The AP asked the government for proof that flossing works. The answer: ¯\_(ツ)_/¯

friedman23 5y ago
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.
- darkerside 5y ago
  Science is however great for combatting truthiness. Some things feel so true that the only way to change is to prove it with science.
  - friedman23 5y ago
    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.
  - deleted 5y ago
    [deleted]
- 83457 5y ago
  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 :(

MattPalmer1086 5y ago

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!

Falkon1313 5y ago

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.