[Hercuros]

I also mentioned this in my other post, but the CompCert compiler is a highly non-trivial example of a program verified using dependent types, and which would not really be possible using automated methods. Of course, not very affordable, since it took years of work from people with expert knowledge. But you get what you pay for, although the price isn't worth it for most real programs in industry.

Furthermore, you don't necessarily need to have an intuition about why the program you are working on is correct to formalize it using dependent types. You just need an intuition about a method for CHECKING that the program is correct.

The four-color theorem was proved in Coq, and it required considering over a thousand cases. No one can keep a proof of this magnitude in their head, but that didn't prevent it from being formalized in a proof assistant. What they did was they just formalized the method for checking and then used that. You can similarly formalize the kind of reasoning that a model checker (or any other automated method) does and then use it in your proof assistant.

[pron]

> but the CompCert compiler is a highly non-trivial example of a program verified using dependent types, and which would not really be possible using automated methods.

First of all, it wasn't really verified using dependent types; it was verified in Coq. Coq's theory is, indeed, based on dependent types, but Coq is used more like a traditional proof assistant (HOL or TLA+) than a dependently typed programming language like Agda or Idris.

Second, CompCert, while certainly non-trivial, is also about 1/5 the size of jQuery, which means it's at least one to two orders-of-magnitude away from the average business application.

> You can similarly formalize the kind of reasoning that a model checker (or any other automated method) does and then use it in your proof assistant.

Yes. In the few cases where deductive proofs are used in industry, they're often used to tie together results from model checking.