6 ms·

Testing / verification is the hardest problem in computing. I don’t think the author actually understands why that is and has a few superficial gripes with how

Testing / verification is the hardest problem in computing. I don’t think the author actually understands why that is and has a few superficial gripes with how codebase are tested. That’s not to say that a lot of test suites are actually good (they’re not). That criticism may be fair. Static types do not help at all with software quality, beyond catching some typos. You can never, ever write a static type that enforces anything of substance, because for that to happen you’d need to execute arbitrary code within the compiler (as happens with dependent types, and of course there is the constant fear of undecidable or infinite type checking in that system). The classic example is that there’s an infinite number of functions with type int -> int. The logic of these functions are extremely varied, and the type doesn’t help you at all. Enum types are very useful for knowing what values you are allowed to write, but don’t help with correctness. The author brings up large input spaces, but conveniently leaves out input space partitioning, which any non-novice tester has to employ in their test case management. The category partition method is a fantastic way of covering large swaths of a seemingly infinite input space with relatively few tests. Of course there’s combinatorial explosion, but that can be mitigated with constraints on the input combinations. I’m not saying testing is perfect - it’s not. But, the burden of proof is on the critic of testing, not testing itself. How else can you reliably change a large software product dozens of times a week, for 20 years in a row? And what’s the alternative when I see products that large teams produce break weekly? This is not something that “ship it and iterate” has had any meaningful impact on. Eventually you get people who don’t intimately know the whole codebase, and make a breaking change unintentionally. What is the alternative to some kind of testing?

sbergot 6y ago
The part about static types is weird. "Tests are not always perfect but can be useful. However static types are not perfect and so they are useless."
- amw-zero 6y ago
  I said that they can catch typos. They’re not generally useless, they are just useless with respect to software correctness.
  - nh2 6y ago
    This is evidently false. It is a well-known result of Computer Science how static types and mathematical proofs are equivalent (see https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...). If you make static types sufficiently good, you get a full theorem prover to prove mathematical properties. There is a whole family of modern programming languages used in verification that exploit this; for example, Agda, Idris and Coq are all practical theorem provers built on static types. If you want to go half the way, try Haskell, where you can express slightly less (but still many) correctness requirements with static types, while still maintaining quite easy ergonomics. If you would like to learn more about theorem proving with Haskell in particular, there is an online 3-hour workshop at MuniHac on "Liquid Haskell" in 3 hours (see https://munihac.de/2020.html#programme https://munihac.de/2020.html#programme). It's free and may change your opinion on software correctness significantly.
    - amw-zero 6y ago
      You either misunderstood or misstated the Curry-Howard isomorphism. Types correspond to _propositions_, programs themselves correspond to proofs. Now, that is one hell of a correspondence and I don’t mean to downplay it at all. But the reason why this isn’t practical in daily programming is that a type represents a set, so all that the isomorphism gets you is knowing that given a member of one type as input you get a member of another type as the output. _Any_ member. This is the problem - the difficulty in verifying logic is showing that the correct output _value_ is given for all input values. Trust me, I have played with Coq for quite a while. Realizing this is what made me abandon the belief that types are some kind of savior. They can be useful, but the program (or proof) itself is what is difficult to get right. I rarely return the wrong type from a function.
      - exdsq 6y ago
        Have you looked into type-driven development? This lets you put your domain model into the type system, potentially add logic if you have dependent types (Idris), and helps a lot with catching issues compared to a dynamic language.
- carlmr 6y ago
  I had the same reaction. Static types can provide very good constraints, obviating a lot of testcases, also they provide a lot of implicit interface documentation when done well. I really like this talk: https://fsharpforfunandprofit.com/ddd/ https://fsharpforfunandprofit.com/ddd/
  - KingOfCoders 6y ago
    I've used a lot of tag types in scala to document and constrain interfaces and liked it a lot.
- fgonzag 6y ago
  I felt the same about it. Static typing is a tool, just like unit testing, integration testing, and code reviews. We combine these tools in order to maximize software quality, ease of development and maintenance. Static typing eliminates a whole class of errors that good code bases in dynamic languages usually have to manually test (instance and type tests)
  - amw-zero 6y ago
    There is no need to have “type” tests in dynamically typed languages. Dynamically typed objects are implementation details, you test without referring to the underlying types. Also, static types _are_ manual testing, you need to write the types.
etripe 6y ago
> The classic example is that there’s an infinite number of functions with type int -> int But are they really int to begin with, as in actually ratio values? Perhaps you're inputting the units requested and getting units available back, which will be completely different from a function that takes an int for the items currently in the basket and returns a new total of items in the basket. Can you compose all those functions into each other? If not, they're not really using the same type but you're representing them as such. That would be undesired behaviour you can totally avoid through subtypes StockAmount and BasketItems. Edit: If you're talking about the math domain, obviously subtyping doesn't apply.
- bluGill 6y ago
  Unfortunately most languages (not all!) don't have a good subtype system. In C++ (or python) I can create a StockAmount class, but since this behaves like an int I have to write something like 30 operators by hand, they all have an obvious implementation but there isn't a good way to get them automatically. The I have to do the same thing with BasketItems. At least C++ lets you make a class that looks like an int, I don't know how you would do this in C, even Java doesn't have operator+ (or didn't last time I used it) I've been thinking about writing a proposal for C++. Problem isn't easy to find something worth writing. Either it is obviously too simple to fit my needs, or it is so complex that I wouldn't accept it if I were on the committee - and this the thought exercise stage where true rigor of reasoning hasn't been applied.
chriswarbo 6y ago
> Static types do not help at all with software quality, beyond catching some typos I strongly disagree. A type like 'NonEmptyList(A) -> B' gives us more information than 'List(A) -> B': in programming terms it eliminates the empty case; in logical terms it provides a proof of 'A'. Note that we can represent 'NonEmptyList(A)' using 'Pair(A, List(A))', but give it a nicer list-like API. Even simple nominal typing can provide useful guarantees, e.g. 'query : String' allows SQL injection, which we can eliminate by defining a separate 'SQL' type. We can represent 'SQL' using a string (we can even make it zero-cost using 'newtype', 'AnyVal', etc.), but crucially we can restrict its API to only allow safe operations, e.g. we can guarantee that strings are escaped by making the escaping function the only way to convert 'String' to 'SQL'; this also prevents double-escaping, since we we can't pass 'SQL' into the escaping function). The exact same technique prevents any injection attack (shell injection, 'eval', etc.). Maybe such things could be called 'typos', but that's just a rhetorical sleight-of-hand; if injection attacks are typos then typos are incredibly dangerous (e.g. https://nakedsecurity.sophos.com/2018/02/19/hackers-sentenced-for-sql-injections-that-cost-300-million https://nakedsecurity.sophos.com/2018/02/19/hackers-sentence... ). We could say static types are great for software quality, since they can even catch typos (which, as we've established, are incredibly dangerous)!
chriswarbo 6y ago
> The classic example is that there’s an infinite number of functions with type int -> int. The logic of these functions are extremely varied, and the type doesn’t help you at all. Yet there is precisely one function with type 'forall a. a -> a', so the type guarantees it's the identity function. Likewise there are precisely two functions with type 'forall a. a -> a -> a': the type guarantees that it will return one of its two arguments (it's equivalent to branching on a boolean). The same pattern holds for selecting between any number of values (which can be useful if we need our caller to make a choice for us). Type constraints are also useful for proving guarantees about our code; e.g. if we have a function like 'forall a. List(a) -> List(a)' then it could do all sorts of rearranging of the elements; whereas 'forall f a. Poppable(f) => f(a) -> f(a)' can only use functions provided by 'Poppable' (presumably: popping elements off the start). We can still pass around 'List(a)' values, as long as 'List' implements 'Poppable', but (a) we guarantee more about the behaviour of these functions (b) the functions are easier to write (since there are fewer things we can get wrong) and (c) the functions are more generic than using a concrete type like 'List'. Note that constraints provide stronger guarantees than subtypes or interfaces, e.g. in Scala 'Poppable[A] => Poppable[A]'. The latter doesn't force the input and output types to be the same, so returning an empty 'List' will work; whereas the constraint requires we return an 'f(a)' for all possible 'f'; hence we're forced to use the input value (in the same way that 'forall a. a -> a' forces us to return the input). Of course, constraints can always be desugared into dictionary passing (e.g. http://www.haskellforall.com/2012/05/scrap-your-type-classes.html http://www.haskellforall.com/2012/05/scrap-your-type-classes... ); e.g. 'forall f a. (f a -> (a, f a)) -> f a -> f a', where the '(f a -> (a, f a))' argument is some sort of 'pop' function; however, we still benefit from static types to ensure that all of these arguments line up (i.e. the same 'f' and 'a' are used in each occurrence), and we benefit from parametricity giving us 'theorems for free' about the possible behaviour.
- amw-zero 6y ago
  None of the constraints you provided are useful in any way. That’s the problem - for some reason people get addicted to the machinery of types, but fail to use them for anything of substance in a real system.
dllthomas 6y ago
> You can never, ever write a static type that enforces anything of substance, because for that to happen you’d need to execute arbitrary code within the compiler (as happens with dependent types, and of course there is the constant fear of undecidable or infinite type checking in that system). Static types are a tool. You can use that tool well, or poorly. There are applications that tool plain doesn't fit. But it is absolutely the case that it can be an important part of enforcing things "of substance" from a very real engineering standpoint (whatever you think of them theoretically). My go-to example from my own experience: I was working on an experimental C project in an environment that demanded minimum latency at low-to-moderate throughput on (expensive) commodity hardware. Our approach was to pin individual threads, dedicated to their task, on individual processors which were otherwise unused. Some functions could only be called on certain threads, usually because some resources could only be accessed from specific threads to avoid locking. Providing an additional argument that labelled the thread let us catch when a change in requirements (which is inevitable when the goal is experimentation) meant logic in the hot path could now be moved somewhere else or what have you. Testing might have turned up race conditions; running them down would likely have been substantial effort. The type system told me "you're calling foo on the wrong thread on line 1234, dummy" and it told me that quickly. None of this is to say we shouldn't be testing - indeed, over the course of the project testing caught a handful of deadlocks the types (at least, those types) couldn't prevent. But the types were invaluable.

sbergot 6y ago

The part about static types is weird. "Tests are not always perfect but can be useful. However static types are not perfect and so they are useless."

amw-zero 6y ago
I said that they can catch typos. They’re not generally useless, they are just useless with respect to software correctness.
- nh2 6y ago
  This is evidently false. It is a well-known result of Computer Science how static types and mathematical proofs are equivalent (see https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...). If you make static types sufficiently good, you get a full theorem prover to prove mathematical properties. There is a whole family of modern programming languages used in verification that exploit this; for example, Agda, Idris and Coq are all practical theorem provers built on static types. If you want to go half the way, try Haskell, where you can express slightly less (but still many) correctness requirements with static types, while still maintaining quite easy ergonomics. If you would like to learn more about theorem proving with Haskell in particular, there is an online 3-hour workshop at MuniHac on "Liquid Haskell" in 3 hours (see https://munihac.de/2020.html#programme https://munihac.de/2020.html#programme). It's free and may change your opinion on software correctness significantly.
  - amw-zero 6y ago
    You either misunderstood or misstated the Curry-Howard isomorphism. Types correspond to _propositions_, programs themselves correspond to proofs. Now, that is one hell of a correspondence and I don’t mean to downplay it at all. But the reason why this isn’t practical in daily programming is that a type represents a set, so all that the isomorphism gets you is knowing that given a member of one type as input you get a member of another type as the output. _Any_ member. This is the problem - the difficulty in verifying logic is showing that the correct output _value_ is given for all input values. Trust me, I have played with Coq for quite a while. Realizing this is what made me abandon the belief that types are some kind of savior. They can be useful, but the program (or proof) itself is what is difficult to get right. I rarely return the wrong type from a function.
    - exdsq 6y ago
      Have you looked into type-driven development? This lets you put your domain model into the type system, potentially add logic if you have dependent types (Idris), and helps a lot with catching issues compared to a dynamic language.
carlmr 6y ago
I had the same reaction. Static types can provide very good constraints, obviating a lot of testcases, also they provide a lot of implicit interface documentation when done well. I really like this talk: https://fsharpforfunandprofit.com/ddd/ https://fsharpforfunandprofit.com/ddd/
- KingOfCoders 6y ago
  I've used a lot of tag types in scala to document and constrain interfaces and liked it a lot.
fgonzag 6y ago
I felt the same about it. Static typing is a tool, just like unit testing, integration testing, and code reviews. We combine these tools in order to maximize software quality, ease of development and maintenance. Static typing eliminates a whole class of errors that good code bases in dynamic languages usually have to manually test (instance and type tests)
- amw-zero 6y ago
  There is no need to have “type” tests in dynamically typed languages. Dynamically typed objects are implementation details, you test without referring to the underlying types. Also, static types _are_ manual testing, you need to write the types.

etripe 6y ago

> The classic example is that there’s an infinite number of functions with type int -> int But are they really int to begin with, as in actually ratio values? Perhaps you're inputting the units requested and getting units available back, which will be completely different from a function that takes an int for the items currently in the basket and returns a new total of items in the basket. Can you compose all those functions into each other? If not, they're not really using the same type but you're representing them as such. That would be undesired behaviour you can totally avoid through subtypes StockAmount and BasketItems. Edit: If you're talking about the math domain, obviously subtyping doesn't apply.

bluGill 6y ago
Unfortunately most languages (not all!) don't have a good subtype system. In C++ (or python) I can create a StockAmount class, but since this behaves like an int I have to write something like 30 operators by hand, they all have an obvious implementation but there isn't a good way to get them automatically. The I have to do the same thing with BasketItems. At least C++ lets you make a class that looks like an int, I don't know how you would do this in C, even Java doesn't have operator+ (or didn't last time I used it) I've been thinking about writing a proposal for C++. Problem isn't easy to find something worth writing. Either it is obviously too simple to fit my needs, or it is so complex that I wouldn't accept it if I were on the committee - and this the thought exercise stage where true rigor of reasoning hasn't been applied.

chriswarbo 6y ago

> Static types do not help at all with software quality, beyond catching some typos I strongly disagree. A type like 'NonEmptyList(A) -> B' gives us more information than 'List(A) -> B': in programming terms it eliminates the empty case; in logical terms it provides a proof of 'A'. Note that we can represent 'NonEmptyList(A)' using 'Pair(A, List(A))', but give it a nicer list-like API. Even simple nominal typing can provide useful guarantees, e.g. 'query : String' allows SQL injection, which we can eliminate by defining a separate 'SQL' type. We can represent 'SQL' using a string (we can even make it zero-cost using 'newtype', 'AnyVal', etc.), but crucially we can restrict its API to only allow safe operations, e.g. we can guarantee that strings are escaped by making the escaping function the only way to convert 'String' to 'SQL'; this also prevents double-escaping, since we we can't pass 'SQL' into the escaping function). The exact same technique prevents any injection attack (shell injection, 'eval', etc.). Maybe such things could be called 'typos', but that's just a rhetorical sleight-of-hand; if injection attacks are typos then typos are incredibly dangerous (e.g. https://nakedsecurity.sophos.com/2018/02/19/hackers-sentenced-for-sql-injections-that-cost-300-million https://nakedsecurity.sophos.com/2018/02/19/hackers-sentence... ). We could say static types are great for software quality, since they can even catch typos (which, as we've established, are incredibly dangerous)!

chriswarbo 6y ago

> The classic example is that there’s an infinite number of functions with type int -> int. The logic of these functions are extremely varied, and the type doesn’t help you at all. Yet there is precisely one function with type 'forall a. a -> a', so the type guarantees it's the identity function. Likewise there are precisely two functions with type 'forall a. a -> a -> a': the type guarantees that it will return one of its two arguments (it's equivalent to branching on a boolean). The same pattern holds for selecting between any number of values (which can be useful if we need our caller to make a choice for us). Type constraints are also useful for proving guarantees about our code; e.g. if we have a function like 'forall a. List(a) -> List(a)' then it could do all sorts of rearranging of the elements; whereas 'forall f a. Poppable(f) => f(a) -> f(a)' can only use functions provided by 'Poppable' (presumably: popping elements off the start). We can still pass around 'List(a)' values, as long as 'List' implements 'Poppable', but (a) we guarantee more about the behaviour of these functions (b) the functions are easier to write (since there are fewer things we can get wrong) and (c) the functions are more generic than using a concrete type like 'List'. Note that constraints provide stronger guarantees than subtypes or interfaces, e.g. in Scala 'Poppable[A] => Poppable[A]'. The latter doesn't force the input and output types to be the same, so returning an empty 'List' will work; whereas the constraint requires we return an 'f(a)' for all possible 'f'; hence we're forced to use the input value (in the same way that 'forall a. a -> a' forces us to return the input). Of course, constraints can always be desugared into dictionary passing (e.g. http://www.haskellforall.com/2012/05/scrap-your-type-classes.html http://www.haskellforall.com/2012/05/scrap-your-type-classes... ); e.g. 'forall f a. (f a -> (a, f a)) -> f a -> f a', where the '(f a -> (a, f a))' argument is some sort of 'pop' function; however, we still benefit from static types to ensure that all of these arguments line up (i.e. the same 'f' and 'a' are used in each occurrence), and we benefit from parametricity giving us 'theorems for free' about the possible behaviour.

amw-zero 6y ago
None of the constraints you provided are useful in any way. That’s the problem - for some reason people get addicted to the machinery of types, but fail to use them for anything of substance in a real system.

dllthomas 6y ago

> You can never, ever write a static type that enforces anything of substance, because for that to happen you’d need to execute arbitrary code within the compiler (as happens with dependent types, and of course there is the constant fear of undecidable or infinite type checking in that system). Static types are a tool. You can use that tool well, or poorly. There are applications that tool plain doesn't fit. But it is absolutely the case that it can be an important part of enforcing things "of substance" from a very real engineering standpoint (whatever you think of them theoretically). My go-to example from my own experience: I was working on an experimental C project in an environment that demanded minimum latency at low-to-moderate throughput on (expensive) commodity hardware. Our approach was to pin individual threads, dedicated to their task, on individual processors which were otherwise unused. Some functions could only be called on certain threads, usually because some resources could only be accessed from specific threads to avoid locking. Providing an additional argument that labelled the thread let us catch when a change in requirements (which is inevitable when the goal is experimentation) meant logic in the hot path could now be moved somewhere else or what have you. Testing might have turned up race conditions; running them down would likely have been substantial effort. The type system told me "you're calling foo on the wrong thread on line 1234, dummy" and it told me that quickly. None of this is to say we shouldn't be testing - indeed, over the course of the project testing caught a handful of deadlocks the types (at least, those types) couldn't prevent. But the types were invaluable.