[thatoneengineer]

Ideally, if you can convince yourself something cannot happen, you can also convince the compiler, and get rid of the branch entirely by expressing the predicate as part of the type (or a function on the type, etc.)

Language support for that varies. Rust is great, but not perfect. Typescript is surprisingly good in many cases. Enums and algebraic type systems are your friend. It'll never be 100% but it sure helps fill a lot of holes in the swiss cheese.

Because there's no such thing as a purely internal error in a well-constructed program. Every "logic error" has to bottom out in data from outside the code eventually-- otherwise it could be refactored to be static. Client input is wrong? Error the request! Config doesn't parse? Better specify defaults! Network call fails? Yeah, you should have a plan for that.

[dmurray]

Not every piece of logic lends itself to being expressed in the type system.

Let's say you're implementing a sorting algorithm. After step X you can be certain that the values at locations A, B, and C are sorted such that A <= B <= C. You can be certain of that because you read the algorithm in a prestigious journal, or better, you read it in Knuth and you know someone else would have caught the bug if it was there. You're a diligent reader and you've convinced yourself of its correctness, working through it with pencil and paper. Still, even Knuth has bugs and perhaps you made a mistake in your implementation. It's nice to add an assertion that at the very least reminds readers of the invariant.

Perhaps some Haskeller will pipe up and tell me that any type system worth using can comfortably describe this PartiallySortedList<A, B, C>. But most people have to use systems where encoding that in the type system would, at best, make the code significantly less expressive.

[josephg]

Yes, this has been my experience too! Another tool in the toolbox is property / fuzz testing. Especially for data structures, and anything that looks like a state machine. My typical setup is this:

1. Make a list of invariants. (Eg if Foo is set, bar + zot must be less than 10)

2. Make a check() function which validates all the invariants you can think of. It’s ok if this function is slow.

3. Make a function which takes in a random seed. It initializes your object and then, in a loop, calls random mutation functions (using a seeded RNG) and then calls check(). 100 iterations is usually a good number.

4. Call this in an outer loop, trying lots of seeds.

5. If anything fails, print out the failing seed number and crash. This provides a reproducible test so you can go in and figure out what went wrong.

If I had a penny for every bug I’ve found doing this, I’d be a rich man. It’s a wildly effective technique.

[rmunn]

This is indeed a great technique. The only way it could be improved is to expand on step 3 by keeping a list of the random mutation functions called and the order in which they were called, then if the test passes you throw that list away and generate a new list with the next seed. But if the test fails then you go through the following procedure to "shrink" the list of mutations down to a minimal (or nearly minimal) repro:

1. Drop the first item in the list of mutations and re-run the test. 2. If the test still fails and the list of mutations is not empty, goto step 1. 3. If the test passes when you dropped the first item in the mutation list, then that was a key part of the minimal repro. Add it to a list of "required for repro" items, then repeat this whole process with the second (and subsequent) items on the list.

In other words, go through that list of random mutations and, one at a time, check whether that particular mutation is part of the scenario that makes the test fail. This is not guaranteed to reach the smallest possible minimal repro, but it's very likely to reach a smallish repro. Then in addition to printing the failing seed number (which can be used to reproduce the failure by going through that shrinking process again), you can print the final, shrunk list of mutations needed to cause the failure.

Printing the list of mutations is useful because then it's pretty simple (most of the time) to turn that into a non-RNG test case. Which is useful to keep around as a regression test, to make sure that the bug you're about to fix stays fixed in the future.

[TruePath]

There is no inherent benefit in going and expressing that fact in a type. There are two potential concerns:

1) You think this state is impossible but you've made a mistake. In this case you want to make the problem as simple to reason about as possible. Sometimes types can help but other times it adds complexity when you need to force it to fit with the type system.

People get too enamored with the fact that immutable objects or certain kinds of types are easier to reason about other things being equal and miss the fact that the same logic can be expressed in any Turing complete language so these tools only result in a net reduction in complexity if they are a good conceptual match to the problem domain.

2) You are genuinely worried about the compiler or CPU not honoring it's theoretical guarantees -- in this case rewriting it only helps if you trust the code compiling those cases more for some reason.

[chriswarbo]

I think those concerns are straw men. The real concern is that the invariants we rely on should hold when the codebase changes in the future. Having the compiler check that automatically, quickly, and definitively every time is very useful.

This is what TFA is talking about with statements like "the compiler can track all code paths, now and forever."

[wakawaka28]

Sometimes the "error" is more like, "this is a case that logically could happen but I'm not going to handle it, nor refactor the whole program to stop it from being expressable"

[cozzyd]

Until you have a bit flip or a silicon error. Or someone changed the floating point rounding mode.

[mark-r]

Funny you should mention the floating point rounding mode, I actually had to fix a bug like that once. Our program worked fine, until you printed to an HP printer - then it crashed shortly after. It took forever to discover the cause - the printer driver was changing the floating point rounding mode and not restoring it. The fix was to set the mode to a known value each and every time after you printed something.

[swiftcoder]

> Until you have a bit flip

These are vanishingly unlikely if you mostly target consumer/server hardware. People who code for environments like satellites, or nuclear facilities, have to worry about it, sure, but it's not a realistic issue for the rest of us

[Yoric]

Of course, any attempt at safety or security requires defense in depth.

But usually, any effort spent on making one layer sturdy is worth it.