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