[yorwba]

> I don't doubt that strong type systems can catch bugs, I am wondering how their capabilities in catching bugs differ from test suites.

Type systems and test suites are complementary. When a test suite finds a bug, that proves that the program is incorrect for some inputs. When a type system doesn't reject a program, that proves that the program is correct for all inputs.

Which one to use depends on the impact of an error. In the case of a system that controls lots of money, you'll want a guarantee that all inputs lead to a correct balance. That suggests to use a type system.

On the other hand, if you're just writing an app to get data from a website and display it, you can probably afford it if the program doesn't work in some cases. If you can write a generator for realistic input, and check the output, that will give you a probabilistic estimate of correctness.

The main advantage that test suites have over type systems is the kind of properties they can easily check. If you have a test suite that only checks that the output values have the right structure (EDIT: https://news.ycombinator.com/item?id=15137691 points out that part of the Lisk test suite does exactly that), you'd probably benefit even from the C type system. But to formalize the correctness of values, for many programs you'd need a much more powerful type system e.g. using dependent types, that isn't quite so simple to use as writing the equivalent test.

I think a good compromise would be a language that allows you to annotate your types with arbitrary properties, but doesn't complain if it can't type-check them, so long as you write a test. (But it should complain when it can prove that the properties never hold, e.g. using success types, so that you don't waste time writing a test for that.)

[jsnathan]

> When a test suite finds a bug, that proves that the program is incorrect for some inputs. When a type system doesn't reject a program, that proves that the program is correct for all inputs.

> Which one to use depends on the impact of an error. In the case of a system that controls lots of money, you'll want a guarantee that all inputs lead to a correct balance. That suggests to use a type system.

When a test suite passes that proves that the program is correct for a subset of all inputs. But I do not see how the same can be said about a type system.

Types do not usually capture semantics - unless we are talking about something a lot more powerful than what I'm used to seeing in real programming languages.

> I think a good compromise would be a language that allows you to annotate your types with arbitrary properties, but doesn't complain if it can't type-check them, so long as you write a test.

But why do I need types for this? Why can't I just assert the properties outright, writing assertions only in terms of the code interface? It's not the types that tell me what arbitrary properties my code should have!

[yorwba]

> Types do not usually capture semantics - unless we are talking about something a lot more powerful than what I'm used to seeing in real programming languages.

You are right, I should have specified that the correctness proof only applies to properties actually given in the type system. So for a high-stakes financial application, your types should be strong enough to capture at least elementary arithmetic. This is definitely not something you'd see in a mainstream programming language.

> It's not the types that tell me what arbitrary properties my code should have!

When you give a variable in a program a type, you assert a property for all values that variable will ever take. The converse is also true: for any property you want to express, there is a type system that can encode it. This is called the Curry-Howard correspondence.

Unfortunately, most interesting properties one might want to formalize require either an undecidable type system, or you have to write a bunch of proof code just to convince the type checker that the rest of the code conserves the properties it should. That isn't too different if you'd be doing formal verification for all your code anyway, but it gets annoying when it is enforced everywhere, even when you'd deem it unnecessary otherwise. In that, it is similar to a policy of "unit tests everywhere", which probably catches some bugs, but also leads to lots of boilerplate stating the obvious.