mkckto

Without knowing anything about the specifics of the conjectures that are falling, I wonder if this affair highlights an issue with the quality of the "open conjectures" that are out there.

There are a lot of reasons you might make a conjecture. Perhaps you are motivated by a search for structure: "We suspect that these objects behave like this, therefore we naturally imagine that...". But you might make a conjecture out of empirical evidence: "We checked 1 million examples, time to make a conjecture." While empiricism has its place in mathematics, it might not be the best motivation for a conjecture. As Bishop said, "Do not ask whether a statement is true until you know what it means." If you pose a conjecture based on empirical evidence, perhaps you should be thinking more about why you would imagine your statement be true in the first place.

I know some will think that this rings of goalpost moving, but when I hear about all these counterexamples spelling the end of mathematics as we know it, I just wonder how strong those conjectures really were in the first place. Again, I haven't actually dug into the specifics of any of the results so admittedly I could be totally off base, but I do know that not all conjectures are created equal.

I think this article highlights a misconception that type skeptics often have, which is that type systems are some sort of enterprise solution that cargo-cultists have come to embrace as "best practices". Either that, or that type enthusiasts are just people that love wearing hairshirts.

Maybe there are some people like that, but for many, types simply are the best way to think about and structure code. They provide a sort of interactive feedback loop that actually makes the development process more pleasant. And these skeptics seem entirely incapable of conceiving that people pick types not because they were looking for some sort of organizational "solution" but because they genuinely prefer the mode of code-writing that type systems enable.