Plausibly, there could be plenty of cases for favoring runtime assertions over dependent types. Or for mixing and matching even in cases where one or the other

Plausibly, there could be plenty of cases for favoring runtime assertions over dependent types. Or for mixing and matching even in cases where one or the other would probably suffice. - Dependent types aren't easily available everywhere. If you don't have them then you can't use them. - The compiler can't prove some statements (admittedly not a big issue for the examples from TFA). Supposing you have a dependent type system which allows you to state that a property holds, it could still be prudent to have a runtime check. If the type system doesn't allow such statements then it isn't sufficiently expressive to solve the problem in the first place. - Assertions are a local change which one can make incrementally, whereas changing the types being used will immediately require larger changes (if the types are used more than once) or necessitate some extra wrapper code.