I’ve never heard that you can program in functional languages without doing testing and relying only on type checking to ensure correct behavior.
“Certain classes of errors” is meant to be read as a very narrow claim, and I’m not sure that it’s relevant to AI design / moral issues. Many sorts of philosophical errors seem to be type errors, but it’s not obvious that typechecking is the only solution to that. I was primarily drawing on this bit from Programming in Scala, and in rereading it I realize that they’re actually talking about static type systems, which is an entirely separate thing. Editing.
Verifiable properties. Static type systems can prove the absence of certain run-time errors. For instance, they can prove properties like: booleans are never added to integers; private variables are not accessed from outside their class; functions are applied to the right number of arguments; only strings are ever added to a set of strings.
Other kinds of errors are not detected by today’s static type systems. For instance, they will usually not detect non-terminating functions, array bounds violations, or divisions by zero. They will also not detect that your program does not conform to its specification (assuming there is a spec, that is!). Static type systems have therefore been dismissed by some as not being very useful. The argument goes that since such type systems can only detect simple errors, whereas unit tests provide more extensive coverage, why bother with static types at all? We believe that these arguments miss the point. Although a static type system certainly cannot replace unit testing, it can reduce the number of unit tests needed by taking care of some properties that would otherwise need to be tested. Likewise, unit testing can not replace static typing. After all, as Edsger Dijkstra said, testing can only prove the presence of errors, never their absence.[14] So the guarantees that static typing gives may be simple, but they are real guarantees of a form no amount of testing can deliver.
“Certain classes of errors” is meant to be read as a very narrow claim, and I’m not sure that it’s relevant to AI design / moral issues. Many sorts of philosophical errors seem to be type errors, but it’s not obvious that typechecking is the only solution to that. I was primarily drawing on this bit from Programming in Scala, and in rereading it I realize that they’re actually talking about static type systems, which is an entirely separate thing. Editing.
Ok, sorry for being nitpicky.
In case it wasn’t clear, thanks for nitpicking, because I was confused and am not confused about that anymore.