| > to separate specification from verification Exactly. Program logics are superior in this regard: the encourage rather than inhibit separation of concerns. (Not to mention: program logics are more developed and cover a large class of computing paradigms, while dependent types have not grown much beyond the pure functions ghetto.) I put forward this point to dependent types luminaries all the time. Its difficult to get more than polite silence in response. * * *
It's partly a social problem: The community working on dependently typed languages and tools typically have most of their programming experience with pure functional languages. Exaggerating only a bit, here is the typical trajectory of a formal methods researcher:- As an undergraduate writes a lambda-calculus interpreter in Lisp/Scheme/Racket/Haskell - As a PhD Student writes their own pure language with wacky typing system, and demonstrate its usefulness by embedding a lambda-calculus interpreter in it. - As a postdoc verifies a lambda-calculus interpreter in Coq/Agda. - As an assistant professor writes their own Curry-Howard-based interactive prover in some dependently typed language and demonstrate its usefulness by verifying a lambda-calculus interpreter in it. - After tenure, gets their students to do the above. 2018's POPL has a type-theory in type-theory paper, but none on how programming language theory can improve SAT solving ... It's an echo chamber. I recently reviewed a grant proposal by some of the more famous dependent types researchers. They proposed using HoTT to verify computational effects. The grant proposal claimed (1) that there is currently no known way to verify effectful languages and (2) that embedding generalisations of effect monads in HoTT is the way to overcome this problem. It seems like these people have not ever heard of program logics? * * *
A second reason is more serious: the real problem of formal verification is not this-language/that-logic.
In day-to-day verification, it doesn't really matter that much
whether you are using this/that approach. You need to set up the right
definitions and invariants. That's the hard part. Whether you express
them in some program logic or dependently typed system doesn't matter
much, you can usually transliterate between them.The real problem is automation. Better autmation means dramatically better SAT solvers (modern SMT solvers are heavily reliant of SAT solvers). It's just unclear where 10x, 100x, 1000x speedups in SAT solvers should come from. We don't even know how to parallelise SAT solvers well. In the absence of dramatic progress in SAT solvers, what can we do other than tinkering with dependently typed languages and their relatives? |
That's a programming language theory researcher. The vast majority of formal methods research is done neither using dependent types nor lambda calculus (and the vast majority of formal tools are similarly neither based on types nor on lambda calculus). However, I do agree that practitioners (i.e., programmers) who become interested in formal methods through functional programming, tend to miss out on the vast majority of progress in formal methods, which isn't related to functional programming at all, and indeed, is normally done in formalisms other than the lambda calculus (which introduces problems related to the common use of higher-order functions, which make some of the clever automation methods harder to apply). They also become familiar with equational reasoning, which works well in pure functional programs, and aren't aware of the more generally-applicable (and arguably more useful) assertional reasoning, which works well even in mainstream imperative languages. They may be aware of assertions, but may not know that their use is actually a formal method of sorts and is an application of Hoare logic.
> Better autmation means dramatically better SAT solvers (modern SMT solvers are heavily reliant of SAT solvers). It's just unclear where 10x, 100x, 1000x speedups in SAT solvers should come from. We don't even know how to parallelise SAT solvers well.
The problem is worse: we don't even know why SAT solvers work in practice at all.
> In the absence of dramatic progress in SAT solvers, what can we do other than tinkering with dependently typed languages and their relatives?
Well, much of formal methods research is done in the field of abstract interpretation (which forms the core of most sound static analysis tools). There is still a lot of interesting progress to be made there. Separation logic is an example of such relatively recent (and important!) progress.