7 ms·

It's a sub-pattern of "ain't got time for dat". Developer knows that condition should never happen, but is not inclined to prove it (as represented by coding ty

It's a sub-pattern of "ain't got time for dat". Developer knows that condition should never happen, but is not inclined to prove it (as represented by coding type checking or other handling) yet realizes it shouldn't be ignored outright (if only to document the unproven condition in code, or to shut the compiler up about incompleteness warnings).

pron 11y ago
> is not inclined to prove it (as represented by coding type checking or other handling) This is known as a reachability problem that in the general case cannot be proven. So, "not inclined" may actually mean "can't (in any reasonable amount of time)".
- dasil003 11y ago
  I came to say much the same thing, but even take it a step further and point out that proofs are subject to human error as well. More powerful programming constructs are a great tool, but at some point it's turtles all the way down. The Knuth quote comes to mind: "Beware of bugs in the above code; I have only proved it correct, not tried it."
- semi-extrinsic 11y ago
  It's not "in any reasonable amount of time". Proving in the general case whether a variable is unused in code or not is equivalent to solving the halting problem. This follows from Rice's theorem: https://en.wikipedia.org/wiki/Rice%27s_theorem#Proof_by_reduction_to_the_halting_problem https://en.wikipedia.org/wiki/Rice%27s_theorem#Proof_by_redu...
  - pron 11y ago
    Yes, but it's more nuanced than that. Even if you can prove that a computation always terminates you can't necessarily prove that it yields the wanted result in any reasonable amount of time. This is the bounded halting problem, and it applies even to languages that only allow terminating computations. In those languages, the halting problem is nominally gone, but the bounded halting problem is just as bad as for Turing-complete languages. Just how bad is it? It is a time complexity class that includes all time complexity classes, i.e. it is harder (in general) than any problem that is computable and known to complete within f(n) steps, where n is the size of the input and f is any computable function.
spdionis 11y ago
Except that you never know how the code you wrote in a module will be used by other developers in the future. Such defensive programming will a least help others prevent mistakes when using your code.
someguy1234 11y ago
Sometimes you do it because the compiler insists a case (that really can never happen) needs to be handled. It happens a lot to me in Rust and Go.
- masklinn 11y ago
  Rust has support for "this can not happen" in core: http://doc.rust-lang.org/core/macro.unreachable!.html http://doc.rust-lang.org/core/macro.unreachable!.html GCC also has an extension for that: https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html#index-g_t_005f_005fbuiltin_005funreachable-4214 https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html#index... which Clang supports: http://clang.llvm.org/docs/LanguageExtensions.html#builtin-unreachable http://clang.llvm.org/docs/LanguageExtensions.html#builtin-u...
  - cpeterso 11y ago
    Note that gcc and clang's __builtin_unreachable() are optimization pragmas, not assertions. If control actually reaches a __builtin_unreachable(), your program doesn't necessarily abort. Terrible things can happen such as switch statements jumping into random addresses or functions running off the end without returning: https://raw.githubusercontent.com/bjacob/builtin-unreachable-study/master/notes https://raw.githubusercontent.com/bjacob/builtin-unreachable...
    - nightpool 11y ago
      Sure, these aren't for defensive programming—they're for places where you know a location is unreachable, but your compiler can't prove it for you. The example given in the rust docs, for example, is a match clause with complete guard arms (i.e. if n < 0 and if n >= 0).
Aaargh20318 11y ago
It's also for cases when you know it can't happen. For example, Java's String class has a method public byte[] getBytes(String charsetName) throws UnsupportedEncodingException Since it can throw a checked exception you have to catch it, which generally is fine, but consider this case: someString.getBytes("UTF-8"); This call can never fail (support for UTF-8 encoding is required in Java) but in my case I have to do something with the exception in the catch statement or our static code analysis tool will start complaining (and rightfully so). So that's where I'll log a 'can't happen error'. It truly cannot happen.
- masklinn 11y ago
  FWIW getBytes(Charset) doesn't throw, and there's a base set of charsets in StandardCharsets (1.7+): someString.getBytes(StandardCharsets.UTF_8); (Charset.forName doesn't throw either, StandardCharsets avoid stringly-typed code but it's not available on 1.6 so if you're still stuck there Charset.forName works)
  - jdmichal 11y ago
    You see the same thing with cipher suites, and there's unfortunately no `StandardCiphers` class.
  - Aaargh20318 11y ago
    yeah I know, this was just the first example that came to mind.
- jdmichal 11y ago
  Also in Java: Switching or if-else chains on an `enum`. It's still a good practice to include a final `else` or `default` case, but it should really never happen. Actually, inclusion of the `default` case will be enforced by the compiler if it can detect a code path that doesn't return. [0] enum Whatever { FOO, BAR } if (whatever == FOO) { } else if (whatever == BAR) { } else { // Should never happen! } [0] http://stackoverflow.com/questions/5013194/why-is-default-required-for-a-switch-on-an-enum-in-this-code http://stackoverflow.com/questions/5013194/why-is-default-re...
kbenson 11y ago
Well, it's used in many, many ways and places, and that's one of them. Often, I'm using it after a two or more branch decision tree, where each branch returns. If someone refactors the code at some point and removes a return, or changes the condition to allow a case to fall through, it catches that. You could be inclined to see it as "is not inclined to prove it", but I prefer to think it happens mostly because someone didn't think they changed something that could affect that (i.e. "I was sure that simple change to the boolean expression was equivalent when I made it...")
frostymarvelous 11y ago
Brilliant response.
eternalban 11y ago
> It's a sub-pattern of "ain't got time for dat". Disagree on this. It has nothing to do with efficiency in context of unlikely events. As others have noted here, it is effectively an assertion of expected language/system/operating-environment properties. Think axioms.
- ctdonath 11y ago
  No, I'm primarily thinking of "ain't got time for dat", as in "there's a very real deadline, I have a lot of other things to get done, and this case isn't ever going to happen and I don't have time to prove it to the compiler."

pron 11y ago

> is not inclined to prove it (as represented by coding type checking or other handling) This is known as a reachability problem that in the general case cannot be proven. So, "not inclined" may actually mean "can't (in any reasonable amount of time)".

dasil003 11y ago
I came to say much the same thing, but even take it a step further and point out that proofs are subject to human error as well. More powerful programming constructs are a great tool, but at some point it's turtles all the way down. The Knuth quote comes to mind: "Beware of bugs in the above code; I have only proved it correct, not tried it."
semi-extrinsic 11y ago
It's not "in any reasonable amount of time". Proving in the general case whether a variable is unused in code or not is equivalent to solving the halting problem. This follows from Rice's theorem: https://en.wikipedia.org/wiki/Rice%27s_theorem#Proof_by_reduction_to_the_halting_problem https://en.wikipedia.org/wiki/Rice%27s_theorem#Proof_by_redu...
- pron 11y ago
  Yes, but it's more nuanced than that. Even if you can prove that a computation always terminates you can't necessarily prove that it yields the wanted result in any reasonable amount of time. This is the bounded halting problem, and it applies even to languages that only allow terminating computations. In those languages, the halting problem is nominally gone, but the bounded halting problem is just as bad as for Turing-complete languages. Just how bad is it? It is a time complexity class that includes all time complexity classes, i.e. it is harder (in general) than any problem that is computable and known to complete within f(n) steps, where n is the size of the input and f is any computable function.

spdionis 11y ago

Except that you never know how the code you wrote in a module will be used by other developers in the future. Such defensive programming will a least help others prevent mistakes when using your code.

someguy1234 11y ago

Sometimes you do it because the compiler insists a case (that really can never happen) needs to be handled. It happens a lot to me in Rust and Go.

masklinn 11y ago
Rust has support for "this can not happen" in core: http://doc.rust-lang.org/core/macro.unreachable!.html http://doc.rust-lang.org/core/macro.unreachable!.html GCC also has an extension for that: https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html#index-g_t_005f_005fbuiltin_005funreachable-4214 https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html#index... which Clang supports: http://clang.llvm.org/docs/LanguageExtensions.html#builtin-unreachable http://clang.llvm.org/docs/LanguageExtensions.html#builtin-u...
- cpeterso 11y ago
  Note that gcc and clang's __builtin_unreachable() are optimization pragmas, not assertions. If control actually reaches a __builtin_unreachable(), your program doesn't necessarily abort. Terrible things can happen such as switch statements jumping into random addresses or functions running off the end without returning: https://raw.githubusercontent.com/bjacob/builtin-unreachable-study/master/notes https://raw.githubusercontent.com/bjacob/builtin-unreachable...
  - nightpool 11y ago
    Sure, these aren't for defensive programming—they're for places where you know a location is unreachable, but your compiler can't prove it for you. The example given in the rust docs, for example, is a match clause with complete guard arms (i.e. if n < 0 and if n >= 0).

Aaargh20318 11y ago

It's also for cases when you know it can't happen. For example, Java's String class has a method public byte[] getBytes(String charsetName) throws UnsupportedEncodingException Since it can throw a checked exception you have to catch it, which generally is fine, but consider this case: someString.getBytes("UTF-8"); This call can never fail (support for UTF-8 encoding is required in Java) but in my case I have to do something with the exception in the catch statement or our static code analysis tool will start complaining (and rightfully so). So that's where I'll log a 'can't happen error'. It truly cannot happen.

masklinn 11y ago
FWIW getBytes(Charset) doesn't throw, and there's a base set of charsets in StandardCharsets (1.7+): someString.getBytes(StandardCharsets.UTF_8); (Charset.forName doesn't throw either, StandardCharsets avoid stringly-typed code but it's not available on 1.6 so if you're still stuck there Charset.forName works)
- jdmichal 11y ago
  You see the same thing with cipher suites, and there's unfortunately no `StandardCiphers` class.
- Aaargh20318 11y ago
  yeah I know, this was just the first example that came to mind.
jdmichal 11y ago
Also in Java: Switching or if-else chains on an `enum`. It's still a good practice to include a final `else` or `default` case, but it should really never happen. Actually, inclusion of the `default` case will be enforced by the compiler if it can detect a code path that doesn't return. [0] enum Whatever { FOO, BAR } if (whatever == FOO) { } else if (whatever == BAR) { } else { // Should never happen! } [0] http://stackoverflow.com/questions/5013194/why-is-default-required-for-a-switch-on-an-enum-in-this-code http://stackoverflow.com/questions/5013194/why-is-default-re...

kbenson 11y ago

Well, it's used in many, many ways and places, and that's one of them. Often, I'm using it after a two or more branch decision tree, where each branch returns. If someone refactors the code at some point and removes a return, or changes the condition to allow a case to fall through, it catches that. You could be inclined to see it as "is not inclined to prove it", but I prefer to think it happens mostly because someone didn't think they changed something that could affect that (i.e. "I was sure that simple change to the boolean expression was equivalent when I made it...")

frostymarvelous 11y ago

Brilliant response.

eternalban 11y ago

> It's a sub-pattern of "ain't got time for dat". Disagree on this. It has nothing to do with efficiency in context of unlikely events. As others have noted here, it is effectively an assertion of expected language/system/operating-environment properties. Think axioms.

ctdonath 11y ago
No, I'm primarily thinking of "ain't got time for dat", as in "there's a very real deadline, I have a lot of other things to get done, and this case isn't ever going to happen and I don't have time to prove it to the compiler."