Nobody who knows what they're talking about says that Haskells types (or even Idris/Agda/Coq's types) "preclude bugs" but instead that they "eliminate some clas

Nobody who knows what they're talking about says that Haskells types (or even Idris/Agda/Coq's types) "preclude bugs" but instead that they "eliminate some classes of bugs so long as you don't behave really pathologically". That's a much weaker statement, but still a valuable property.