Software correctness is a lot like flossing (2020)

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.

[1] https://www.manning.com/books/type-driven-development-with-i...

[2] https://www.idris-lang.org/index.html

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.

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.

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.

> 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!)

Science is however great for combatting truthiness. Some things feel so true that the only way to change is to prove it with science.

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 :(