-
依赖类型语言没有能胜任内核开发性能，底层操作要求，实时性要求，又同时满足能找几个到会的人的。比如 Idris 一开始就吹能搞 OS，然后实际 codegen 出来就把宣传变成 Application 了。
-
对性能之类要求不高的话，其实 Coq 本来就主打程序生成。你可以把 Coq 看成一个 dependent types PL。
-
形式化验证和依赖类型是两码。现在硬件和 OS 验证仍然比较流行的 HOL 就是在用 classical logic。选用 Coq 也只是因为生态工具的原因加上那么一点 constructive logic 能生成程序的原因。原则上，即使用 classical logic/Hoare Logic 也能生成程序，dependent type 说不上是什么必须的东西。
说白了你还没理解 dependent type 是什么，为什么要它，只是听说它很先进，PL 都在搞它。