I can’t stop thinking about this comment by abstract_type on the blog:
Tests are entirely useless for correctness guarantees; at best, tests are a description of how some happy path works. Correctness is provided by construction (of a type) and composition (of smaller programs), and the easiest way to enable this is by a sound static type system which acts as a lightweight proof (as opposed to actual theorem provers like Coq, Agda etc).
I feel like this is itself a happy path view of types and type safety: if you just use the right types, everything else falls into place! But my experience with even minimal business software (not side projects) has shown that they can and do contain logic that defies “simply creating a type”. Business logic will always require runtime verification, which is the domain of tests.
The norm in Javascript-land is to write reams of “type” validation tests: was I passed a string? Do I throw if I’m passed a non string? Do I return a number? Etc etc etc. It’s exhausting and from this perspective I can see how a static type system sounds like a panacea. But even given that a static type system would catch those errors up front, having one wouldn’t protect from business logic errors such as appending a user to a list of users instead of pretending them, or incorrectly formatting a string, or performing the wrong query.
I feel like Rich Hickey has talked about this at length but I can’t remember which talk it is. (Maybe Maybe Not?)
It depends how powerful your type system is and how much you use that power. At the limit, a powerful enough type system (dependent types) used to the max can encode everything a unit test can. The happy place is usually some middle ground of course, but if your type system’s only abilities are to describe “is a number” or “is a string” I would say you’re too far down that spectrum for the types to really be useful yet.
I don’t know almost anything about dependent types, so can they solve the issues I described? Can you create a type that encodes a correctly formatted string? Can you create a type that encodes the right query with duplicating the query?
With dependent types, you could write the query as a type and have the implementation be inferred from that type, for example. The types are turing complete and can do anything code can do. That’s not to say you always want to do this of course. I think certain kinds of string formatting (probably the kinds you are thinking of) are not the right place to use type to enforce, personally, but of course we’re not talking about anything concrete here and different people have a different feeling about how far they want their types to go.
I loved reading this article (his blog is fantastic) and I can’t
add anything more than a pet peeve - every time a developer talks
about tests they should really say checks. Unit tests doesn’t
really test anything!
A test is where you explore a hypothesis and see it holds up, and
is performed by a human (until, if ever, AI catches up!). A check
is done by a machine to check facts and happy paths. When I worked
as a software tester I let my experience guide me, and could
change and adapt my testing when new facts showed up during the
run. With a unit test all of this has to be done up front, which
is hard when you try to cover more than the happy path.
Also, a (unit|integration) test can’t ever validate a system, it
can only (reliably) verify it.
Don’t know about you guys, I just pray a lot
🧑💻📿🙏
This Twitter thread is a nice tour of different software correctness approaches.
I can’t stop thinking about this comment by abstract_type on the blog:
I feel like this is itself a happy path view of types and type safety: if you just use the right types, everything else falls into place! But my experience with even minimal business software (not side projects) has shown that they can and do contain logic that defies “simply creating a type”. Business logic will always require runtime verification, which is the domain of tests.
The norm in Javascript-land is to write reams of “type” validation tests: was I passed a string? Do I throw if I’m passed a non string? Do I return a number? Etc etc etc. It’s exhausting and from this perspective I can see how a static type system sounds like a panacea. But even given that a static type system would catch those errors up front, having one wouldn’t protect from business logic errors such as appending a user to a list of users instead of pretending them, or incorrectly formatting a string, or performing the wrong query.
I feel like Rich Hickey has talked about this at length but I can’t remember which talk it is. (Maybe Maybe Not?)
It depends how powerful your type system is and how much you use that power. At the limit, a powerful enough type system (dependent types) used to the max can encode everything a unit test can. The happy place is usually some middle ground of course, but if your type system’s only abilities are to describe “is a number” or “is a string” I would say you’re too far down that spectrum for the types to really be useful yet.
I don’t know almost anything about dependent types, so can they solve the issues I described? Can you create a type that encodes a correctly formatted string? Can you create a type that encodes the right query with duplicating the query?
With dependent types, you could write the query as a type and have the implementation be inferred from that type, for example. The types are turing complete and can do anything code can do. That’s not to say you always want to do this of course. I think certain kinds of string formatting (probably the kinds you are thinking of) are not the right place to use type to enforce, personally, but of course we’re not talking about anything concrete here and different people have a different feeling about how far they want their types to go.
I think the simplest way to put is that tests cover what your type system can’t.
That’s a great, pithy way to put it, thanks. Explains why there are so many ridiculous tests in Javascript-land.
I loved reading this article (his blog is fantastic) and I can’t add anything more than a pet peeve - every time a developer talks about tests they should really say checks. Unit tests doesn’t really test anything!
A test is where you explore a hypothesis and see it holds up, and is performed by a human (until, if ever, AI catches up!). A check is done by a machine to check facts and happy paths. When I worked as a software tester I let my experience guide me, and could change and adapt my testing when new facts showed up during the run. With a unit test all of this has to be done up front, which is hard when you try to cover more than the happy path.
Also, a (unit|integration) test can’t ever validate a system, it can only (reliably) verify it.
Edit: this might be worth reading: https://www.satisfice.com/blog/archives/856