So I've been thinking about the testing vs program verification (type safety etc), how testing can never prove the absence of errors etc. I think these academics are missin out one key point: there is only a finite set of programs that solve a particular problem and don't have superfluous stuff and don't look like gibberish. Right? And with every test you perform, you're narrowing down the space of those programs, and it's possible to arrive with testing at the one unique (up to some equivalence like reordering some shit) program that is correct. On the other hand, type systems and program verification can not really prove the absence of errors either. They only prove what you've had the ingenuity to prove and encode in the type system. Simple example: you're writing a financial accounting program and you've used floating point numbers. Will it typecheck? Yes. Will it behave erroneously? Yes, because you forgot that your AccountSum type must have integer representation, and didn't encode that into the type. The type checker is never smarter than the programmer, it's just more diligent and thorough, that's all. So what I'm getting at here is that testing and program verification are really two different approaches to program correctness and none of them is better or worse than each other. There are cases where testing will cover your ass while Coq won't, and vice versa. So you academics can't really be looking down on us all with your type theory an shit. And there are reasons why dependent types aren't picking up, cause they might be too little bang for the buck and still not 100% guarantee your programs are correct.