Yes I agree with you on every point (though didn’t want to use the “heavy gunner” Collatz as an example :D). I’m not against dependent types, and I eagerly awai

Yes I agree with you on every point (though didn’t want to use the “heavy gunner” Collatz as an example :D). I’m not against dependent types, and I eagerly await what future might they bring. But at the same time I think the best solution will be to “fight on multiple fronts”, and improve our type and test systems. There are very interesting ways to systematically test every kind of input (greatly reducing the input space) that has a distinct code path (and it can find a minimal reproducible error case!).