Symptom Rice’s theorem (T011) told you every non-trivial semantic property is undecidable. Your static analyzer must therefore be unsound, incomplete, or non-terminating. In practice it is incomplete: it reports things that cannot happen. ...
Symptom Someone hands you a function and no source: f :: forall a. [a] -> [a] How much can you say about it? The instinct is nothing: any implementation is possible, that is what polymorphism means. ...
Symptom You write this in OCaml or Haskell and annotate nothing: let rec map f = function | [] -> [] | x :: xs -> f x :: map f xs The compiler reports ('a -> 'b) -> 'a list -> 'b list. It found the most general possible type, on its own, with no hints, and it will reject any call that does not fit. ...
Symptom You write a function signature and it looks like a sentence: f :: (a -> b) -> (b -> c) -> (a -> c) Read it aloud: if $a$ implies $b$, and $b$ implies $c$, then $a$ implies $c$. That is transitivity of implication, a rule of logic you have known since school. And the implementation, f g h = h . g, is the proof of it: given evidence for $a$, apply the first, then apply the second. ...
Symptom You are writing a language, or a configuration evaluator, or a template engine, and you need recursion. So you add a letrec form, and now the evaluator needs to bind a name before the value it names exists. You reach for a mutable cell, a placeholder that gets patched after construction, and something about it feels like cheating. ...
Symptom Every distributed result so far has been a prohibition. Two Generals: no agreement over a lossy channel. FLP: no deterministic asynchronous consensus. Byzantine: not below $3f+1$. CAP: not all three. ...
Symptom The security team asks for a scanner with no false positives and no false negatives. Every piece of malware caught, nothing legitimate quarantined. The platform team asks whether the analyzer can flag every function that performs I/O, so the pure ones can be cached automatically. ...