[dwheeler]

Material implication has its advantages, but it does sometimes lead to errors. That said, there are ways to reduce the problem.

One error is that sometimes people use material implication inside of for-all, and forget that if the antecedent is always false than the entire expression is always true. I specifically created a quantifier called allsome that counters that problem: https://dwheeler.com/essays/allsome.html

Another problem is using material implication inside there is quantifier. That is almost always a mistake, as usually and is meant instead. However, that is pretty easy to detect automatically. Both Why3 and SPARK already attack that.