> 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.

> "wrong type"

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.

This is pretty much my experience as well, including the part about Java programmers.

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

> 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.

> 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.

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.

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.

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

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.

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.

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

ps: Thanks for the upvote :)

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!