TLC checks specifications of arbitrary detail. I don't see why it matters when it comes to deep properties. There does not exist any method -- automated or manual -- that can verify deep properties of code of size even within an order of magnitude of ordinary applications. Inasmuch as model checkers and deductive proofs work at all, model checkers are clearly more scalable.
> But it's not the same as checking 50kloc _programs_, and you should not conflate these activities.
I explicitly said that model checkers don't beat deductive proofs on size and depth at the same time, but they do beat them easily separately. Still, there are a few cases where model checkers fail, and the only option available is formal proof. Usually, that is too expensive, but we have seen that in extreme circumstances when a great amount of work is applied to a very small amount of code, this could "work" in the sense that specialized, highly-trained teams working for a long time could do it. AFAIK, this has so far only been tried in research projects, and never by "ordinary" engineers.
> And what you're competing against (dependent types) has the potential to scale far better: even the 3.5kloc Agda program I'm working on can be checked in under a minute, and Agda is very far from optimal with respect to type checking.
If checking a proof were comparable to finding one, then the P vs NP problem would have been resolved a long time ago. You should compare the time it takes to write and model-check a 3500-line TLA+ spec vs the time it takes to write a 3500 line Agda program and check the proofs.
> Contrary to your earlier claims, there is no agreement in the field that one should "look elsewhere".
I didn't say there was consensus; I said that the majority of researchers are looking elsewhere, and that's where most research is focused.
> But don't act as if it's an empirical fact when the evidence shows no such scalability advantage at this point in time, and most deep properties that deductive, proof-producing methods can establish are still out of reach for non-deductive methods.
Deductive methods have been studied for at least forty years now, and AFAIK, they have never been used in any meaningful scale by non-researchers in industry. On the other hand, while automated methods obviously have not reached the point that they could automatically verify arbitrary properties of arbitrarily sized code -- and they never will, and neither will deductive methods -- they are being used in industry on a regular basis, with capabilities ranging on depth, scale, and soundness, and their use is growing; just in the safety-critical space where SCADE and Simulink are used, but at Microsoft, Amazon, Oracle and Facebook as well as smaller companies. As an applicable formal method in the real world, deductive proofs don't even exist yet, heroic efforts by researchers notwithstanding.
Which is why it's unsurprising that more researchers are looking into methods that have had some measure of success outside research. I find all aspects of formal methods very interesting, and I wish all researchers luck and success (and I sometimes amuse myself with small machine-checked proofs, usually in the TLA+ proof assistant or sometimes in Lean), but it is misleading to present deductive and automated methods as being on equal footings in terms of real-world success.
I also think there is a fundamental mismatch between deductive proofs and software verification, something I call the "soundness problem." Unlike mathematics, while an algorithm can be proven correct, a software system never can, any more than a chair could -- it's a physical system. This means that soundness is never, ever, ever a requirement in software verification. On the other hand, achieving soundness (for deep properties) is very costly, as both theory and experience tell us. This is why many experiments these days -- both in academia and industry -- try to turn down the soundness knob to achieve other actual requirements in software verification (see O'Hearn's recent "incorrectness logic"). A method that is inflexible on soundness -- which is both not required and very costly, is one that seems to be clashing with the very needs of software verification.
This is also why you find that research projects using deductive proofs are almost invariably done by people with little or no industry experience. They treat the problem of software verification as an academic exercise without understanding what real software is and how it's used. On the other hand, you see many more researchers with industry experience looking into automated methods. It's funny, to see the transformation. You look at someone like Peter O'Hearn that's moved from academia to industry. What does he do then? Turn down soundness. You also see it with Leslie Lamport and David Harel, and I could probably find more examples. Once researchers are faced with how software is actually developed, the first thing they realize you need to do is to reduce soundness (for deep properties). Soundness is not a requirement, and it is the enemy of scale and speed, which are (I've written a short post on one aspect where researchers don't understand how software is written: https://pron.github.io/posts/people-dont-write-programs). There are cases in software where soundness is needed -- automatic refactoring and compiler optimization -- which is why I think type systems are interesting for those, but correctness -- not so much.
On the other hands approaches to correctness based on dependent types are favored by people who may be very good researchers, but are not professional programmers, not familiar with industry, and have not conducted field studies (people like Bob Harper, Adam Chlipala, Edwin Brady, and Leonardo de Moura). Now, their research is very good, but it is theoretical, and so far unsuitable for any field use, which is unsurprising, given that they're unfamiliar with how software is made. Which brings me back to my original point: bringing dependent types to Haskell is an interesting first field experiment, but it is just that -- a research experiment designed to answer a research question (someone who worked on seL4 told me that they believe they could bring the cost down enough to be similar to that of high-assurance software, but that's not where Haskell is or, I think, wants to be). It is very different from the kind of work that people like O'Hearn and Lamport are doing, which is scaling up approaches that have already shown their worth in the field.