This is a really bad argument imho. I'm an agda programmer, but only for hobby projects. You can do pretty much everything you listed: "model checking, program analysis, abstract interpretation and type systems" in agda, right now, this very day and some of these stuff is built-in (like dependent type system) or in the standard library. There even is a small industry built around proof automation. But it doesn't follow agda will solve software engineering. When it comes to engineering, it's also about constructing, not just about correctness. Everything you listed solves the latter while ignoring the former. I think the fundamental problem with software engineering is that it is a little too much like mathematics, to the point, the only way to be correct is to be as precise as agda, but, people who practice software engineering, again, just like mathematicians don't care to use this precise language. Just like a mathematician will never write his paper in agda instead of human language, unification will never by itself solve software engineering. Programs are written for humans, not for automated proof checkers, just like papers on mathematics are written for humans.
