This comes down to the concept of 'proof'. How do you know that the code you wrote does what you think it does? You construct some sort of proof in your mind, b

This comes down to the concept of 'proof'. How do you know that the code you wrote does what you think it does? You construct some sort of proof in your mind, but for any non-trivial code you have to follow certain operational rules[1] because you can't hold the whole code in your mind all at once. That is you work on smaller parts of it, proving to yourself that it works like you expect, and put those parts together using operational rules that you just have to assume are correct. Like if you have {f(a,b) => a+b}, you can conclude in your mind that {f(1,2) == 3} (but you're really doing a whole lot of rule-application under the covers). What if the code you wrote gave you guarantees about the things that it did, as long as you trust the compiler/proof-checker/other tools that used to verify the correctness of the code? This is basically what testing does-it gives you proof. As long as the things you test are "pure" or functional in the sense that they will do the same thing every time, given that they are given the same inputs, you have proof that the code is correct. The problem with testing is that you can't test everything because of combinatorial explosion. However, there's a trick to this where you can collapse states together and prove something using that collapsed state. For example, you collapse all 32-bit positive integers {1,2,3,...} into the state {N} and now as long as you prove something that holds for {N} you also proved something that holds for all 2^31-1 positive integers. You just have to be very careful and very precise about what you're doing, and that's where your compiler comes in to help. (So this next part is kinda butchering the math behind it and all sorts of programming language theory, apologies in advance.) You can kind of think of the state {N} as a type [2], and {1,2,3,...} as instantiations of that type. You can do something like "prove" that if you're given {f(a,b) => a+b} and {a=1, b=2} then you can conclude {f(1,2) == 3}, and throw that under some test. The test instantiation where you run 'assertEquals(f(1,2), 3)' is basically a concrete instance of your proof that 'f' does what it should. You just have to trust that your runtime environment is behaving correctly (no bugs). You can also consider functions that can be defined in your language as types (e.g. f: int -> int, a function that takes an int and gives you an int). That's the 'function signature' or 'function declaration'--it's type. And you can consider instantiations of this type to be the same thing as a function definition --where you define what the function does. As long as your function definition doesn't throw any compiler errors (that is, it passes your type-checker and there are no bugs in your toolchain), then you have provided an instance of a proof that the function definition is of the type of the function declaration. This might not sound like much ("great, the function definition has a certain type...didn't we already know that?"), but as long as your function definitions are pure functions (no external state change), you've just guaranteed type safety in your program [3]. Your program will never crash because you input a string when you should've input an int (hello JavaScript...). The type-checker won't allow you to write such a program. You can get a lot more guarantees than what I just mentioned, and there is a ton of active research in this area [4]. So to answer your first question, yes, they are suggesting writing code that you don't necessarily understand because you "offload" parts of your understanding to the compiler (type-checker). It's like when you do an automated refactor--if your code and the auto-refactoring tool are written correctly you can just trust that it did the right thing and doesn't cause any bugs. As for your second question, I can't answer it because I haven't used Haskell. [1] https://en.wikipedia.org/wiki/Operational_semantics https://en.wikipedia.org/wiki/Operational_semantics [2] https://en.wikipedia.org/wiki/Type_theory#Basic_concepts https://en.wikipedia.org/wiki/Type_theory#Basic_concepts [3] https://en.wikipedia.org/wiki/Type_safety https://en.wikipedia.org/wiki/Type_safety [4] https://en.wikipedia.org/wiki/Static_program_analysis https://en.wikipedia.org/wiki/Static_program_analysis