Thread by @ShriramKMurthi

This man literally has no idea what he's talking about. Stay in your lane, dude.

https://twitter.com/unclebobmartin/status/1135894377329508355

I got called out by @paulg for not explaining my comment. Fair point, though sometimes it's exhausting. Maybe that means one unwilling to explain their reasoning shouldn't comment at all. Topic for another day. Let me explain my response a bit here. »

Note that I'm assuming a SOUND type system. (Please look that up. E.g.: Pierce's TAPL or my PLAI [plai.org].) Otherwise many bets are off; depending on level of unsoundness, effectively a dynamic language (or worse). »

A static type system's soundness guarantee tells us that certain bad things simply can't happen. Therefore, not only is there nothing to test, the type system literally won't let you write that ill-typed test to explore outside the space. »

<sidebar>
To play the opposition for a moment, that is also a problem. In an era of hardware attacks, soundness may not quite hold. BUT, this is NOT a type-specific issue. The real fault is a failure of *safety*, not *soundness*. The same problem applies to, say, Ruby/Python. »

They too assume certain bad things can't happen in the runtime. So they won't let you write certain code: e.g., you can't get the address of a closure, go into it, find the environment pointer, and change it. A hardware attack could do that, buy you can't test for it. »

Safety and soundness routinely get conflated and confused. A sound type system invariably depends on a safe runtime. A safe runtime doesn't need a non-trivial type soundness (eg, dynamic languages). »

If you really want to understand this better, Felleisen and I wrote an unpublished paper about this.
www2.ccs.neu.edu/racket/pubs/tr…
</sidebar> [thread resumes »]

So, back to types and tests. A sound type system literally precludes certain behaviors, so the set of tests you write when they are precluded not only can be different, in the extreme, it must be (e.g., you can't write that ill-typed test). »

<sidebar>
This is related to what I feel is a common misunderstanding of what type soundness means. We explain this in our "Progressive Types" paper. Just read the intro.
cs.brown.edu/~sk/Publicatio…
</sidebar> [thread resumes »]

But I can imagine a reader thinking, "Okay, but that's pretty weak sauce". So let me give you two much more interesting examples. »

1. As others have also pointed, parametricity is a case in point. If I have a language with relational parametricity, a parametric type (e.g., forall T . <something involving type T>) is a universal quantifier with a strong guarantee about ALL T. I don't need to test them all. »

Curiously, there's *value* to doing so at multiple types for T, because it provides explanatory power to the reader reading the tests to understand the function (e.g., in docs). In fact, @PyretLang's test-based type inference infers quantifiers from such polymorphic uses! »

Nevertheless, this is a case where the type system literally does change your testing. You CAN (always) write more tests than necessary, but one test of a parametric-typed function literally corresponds to an infinite number of tests without that type guarantee. »

2. Let me move on to a more interesting case. Suppose you're writing a device driver, packet filter, etc. One thing you care about deeply is termination. So one of the things you'd like to test for is termination. »

Termination is fun: runs exactly into proof-vs-testability, as in the original thread. You can't prove it always terminates. You can only run several tests and make sure they all did. You need a timeout. That only says "didn't terminate quickly". May have done so a bit later. »

I feel another sidebar coming on.
<sidebar>
Proving termination is of course impossible (Halting Problem). And I feel the HP is literally the thing that makes CS a truly distinct discipline from any other (eg, math). »

We study processes. They have behavior. Our processes are non-trivial. So non-trivial that Halting is even a question (and important). And so non-trivial that we cannot build a decision procedure for it. It's like our "original sin" that keeps recurring.
</sidebar> [thread»]

Except, of course, that I'm lying and set you up. The HP is undecidable *for a certain language*. You can easily solve the HP if you change the language. One of my fun puzzles in a model checking class is to encode the HP and show that it appears trivially decidable. WAT. »

So let's bring this back to types. One of the canonical languages of study in PL is the Simply-Typed Lambda Calculus (STLC). And the STLC has this glorious property that every program in it is guaranteed to terminate. It enjoys that property *because of the type system*. »

This is a rather awesome result. You can have a pretty powerful language, EVEN with full-fledged lambdas, and no matter what you do, you can't make it go into an infinite loop. (Exercise: try encoding the Y combinator [to bring this back to @paulg] and see what goes wrong.) »

At any rate, I believe this constitutes a definitive refutation: "The number of tests you write and execute is [most certainly affected] by the type system of your language." Before I go … »

If all this is news to you, I suggest reading any of the PL resources mentioned above. You can also get such content from my on-line PL course, with @joepolitz.
cs.brown.edu/courses/cs173/…

Just for the fun of it, I'm going to add TWO MORE interesting type properties! »

3. Ownership/aliasing. If you care about the which objects hold which others (e.g., for resource-mgmt or object capability analysis), you can do this automatically through some modern type systems. Think about testing for that. Now think about NOT having to write those tests. »

4. Non-interference/information flow. The idea here is you want to make sure that high-security data don't flow to low-security entities. Many systems actually have this property (e.g., on a Web site, the password mustn't leak to the Web page). Do you test for these? »

Really interesting: turns out these properties actually belong to a class called "hyperproperties". These are things that can't be checked of a *single* run of a program: they need multiple runs. Essentially: without that, you can't tell if something *leaked* or was legit. »

So there's solid math that says just how hard/impossible (depending on your definition) it is to test such a property. But an information-flow type system gives you this guarantee automatically. Voilà, no need to write those tests. Because of your type system.