> There are various results showing that the difference in size between an informal proof (even when correct, which, as experience shows often isn't[1]) and a formal one may be exponential.
What's the definition of an informal proof, and in what sense can it be exponentially smaller than a formal proof? Even if you can answer this, it sounds as if you are ignoring all the progress we have made in programming language design. The whole reason we have modern programming languages is to bridge the gap between the "informal proof" you keep in your head and an actual formal correctness proof.
For example, C programs typically have a lot of bugs because there is such a large disconnect between the model of the program in your head (which also lacks most of the error states) and the actual state space of the program. Almost every abstraction in C is potentially leaky, and this just doesn't allow you to reason succinctly about your program. This is not even specific to C. The "simple" imperative programming models that are still used almost everywhere have exactly the same problem.
The point of modern programming languages isn't that it's essentially the same thing, but with a scalable static analysis tacked on (types). The point is that we try to impose a discipline on programs which allows for modular correctness proofs. If you have a module implementing a certain data structure in ML, you can reason by parametricity about its correctness and once you have established whatever properties you want, nothing will every break them again. Essentially, you have just taken part of the state space and shrunk it down to a single bit.
And that this is possible is not at all surprising! Everything you write, here or in your article, is also applicable to ordinary mathematics. So if theorem proving is fundamentally difficult, how do we make progress in mathematics? By finding new abstractions and by composing abstractions.
We are making real progress in verification. Nowadays, there are scalable proof techniques for concurrent programs, even in the presence of weak memory models (GPS, iCAP, Iris, ...). There are compositional proof methods for program equivalence which scale to real programming languages (step-indexed logical relations, ...). There are language primitives for safe, efficient and easy to reason about concurrent and distributed programming (e.g., join calculus). And many, many more things which were previously thought of as stupendously complicated.
> What's the definition of an informal proof, and in what sense can it be exponentially smaller than a formal proof?
A formal proof is one that can be mechanically translated to the logic's deduction rules. An informal proof is anything that is considered by mathematicians as proof, yet isn't a formal proof. It is smaller because it skips many details, but seems convincing enough.
> it sounds as if you are ignoring all the progress we have made in programming language design
We have not made significant progress when it comes to proving global logical properties, and I don't think anyone claims we have. There are languages that in theory can be used to prove correctness; in practice they have never been successfully used on real world programs, except for small and simplified ones, and even then with great effort by experts.
> For example, C programs typically have a lot of bugs because...
The reason why many languages are safer than C is because they prevent certain bugs by enforcing local properties, like memory safety. This is an example of a local property (that's easy to prove, even automatically, in many cases) that is known to be the cause of many costly bugs. Other languages don't fare significantly better when it comes to proving global correctness. The best we've done -- and that's not insignificant -- is reduce accidental complexity to proof.
Like I show in my post, even a language with nothing but boolean variables and pure functions -- no memory allocation, no recursion or iteration of any kind and no higher-order functions -- where all programs are obviously terminating and the language is too weak to do anything useful, cannot be feasibly verified in general. Languages can help with local properties. The difficulty of proving logical correctness is dependent almost entirely on one thing: how simple your algorithm is.
> The "simple" imperative programming models that are still used almost everywhere have exactly the same problem.
So far imperative languages seem fare better than FP in terms of verification. Fully verifiable languages that are used for safety-critical realtime systems, are also imperative (although not in the same way JavaScript is).
Make sure that by reading papers in PLT you're not falling into a bias trap. PLT nowadays is mostly concerned with FP, so papers will be on FP. Those who are interested in the verification aspects of PLT, will write about ideas that they think show promise. But most of verification research isn't PLT, and deals with imperative (or language-agnostic) algorithms, and they have their own results, which are no less promising. Neither has been able to "solve" verification in the sense people hoped in the 70s, and AFAIK, neither community is trying to do that. That doesn't stop them from publishing results that are very promising, but haven't been proven in practice yet. But if you're exposed to only one community, you may get the false sense that there is one consensus approach (there isn't), and we're slowly but surely getting to our destination (maybe we are, but we don't know for sure, and we don't know which approach works in practice).
> for modular correctness proofs
The well-known results quoted in my post show that global correctness properties cannot be modularized, nor does anyone claim they can be. Certain properties which could prevent certain bugs can definitely be made easier to prove with modularity -- they're local in some way -- but certainly not global logical correctness. Some people may hope that global correctness would turn out to be decomposable in enough use cases, but this is an empirical conjecture, with little proof so far.
> Essentially, you have just taken part of the state space and shrunk it down to a single bit.
Yes, this is what abstract interpretation does, and types carry it out. But not every property survives this state reduction (most of them don't). The challenge is to figure out which properties that can prevent expensive bugs can be proved.
> So if theorem proving is fundamentally difficult, how do we make progress in mathematics? By finding new abstractions and by composing abstractions.
Theorems proven in math are much deeper yet deal with far simpler concepts than computer programs. The whole idea of computer programs is that they create small structures that defeat mathematical reasoning. It is no accident that Hilbert's program was laid to rest by the "discovery" of computer programs. Like I wrote in the post, we know of specific, positively tiny programs, that are known to elude the power of math completely. The best analogy is physics. The gravity equation is simple, modular, pure, equational, algebraic, composable -- whatever good PL adjective you may hope to assign. It is so simple that it is completely uninteresting to mathematicians. Yet, combine two of those equations together -- they compose very nicely -- and already no closed-form solution exists and the behavior can no longer be predicted; it is uninteresting to mathematicians (well, except for some instances), but for the opposite reasons. Programs are much more like the gravity equation -- made of small simple parts, that may become completely chaotic when combined -- than any mathematical theorem.
> We are making real progress in verification.
Absolutely, but the goals are different. Most of the time we're talking local properties or a lot of effort or restricted domains. Most of the things you mention that are relevant to global properties have so far failed to scale to real-world programs. Affordable proof of ordinary software's global correctness is no longer a goal and certainly not a promise of contemporary software verification.
BTW, most progress in verification is not in PLT. Restricting yourself to PLT is a sure way to miss most of it.
> The well-known results quoted in my post show that global correctness properties cannot be modularized, nor does anyone claim they can be.
You are seriously overselling these results. Here's one way to make termination proofs modular: Take the graph of your function (vertices for each value of the arguments, edges for recursive calls) and take its transitive closure. If you can cover the transitive closure with an arbitrary number of individually well-founded relations, the function terminates.
> Yes, this is what abstract interpretation does, and types carry it out. But not every property survives this state reduction (most of them don't).
The point of having contextual equivalence or a program logic is that every property you can express in your programming language/logic survives this state reduction.
> Like I wrote in the post, we know of specific, positively tiny programs, that are known to elude the power of math completely.
You give an example of a termination problem which is equivalent to the consistency of ZFC. Does the consistency of ZFC "elude the power of math"? It's certainly a very simple question, much easier to write down than the Turing machine in question.
> Programs are much more like the gravity equation -- made of small simple parts, that may become completely chaotic when combined -- than any mathematical theorem.
This applies to mathematics as well. You can write down simple sounding questions, like the Collatz conjecture you mention, which are actually extremely complicated. This is the point where complexity theory comes into the picture. For instance, I could generate random types in the calculus of constructions (random propositions) and ask if that type is inhabited (the proposition is provable). This is an undecidable problem and for complexity theoretic reason most instances (of a certain shape) will actually be hard.
The concepts in programming aren't inherently more complicated than the concepts in mathematics. If anything, there are plenty of natural concepts in mathematics which behave far more chaotically than anything in CS (look at a table of homotopy groups of spheres and tell me where that pattern comes from).
> Most of the things you mention that are relevant to global properties have so far failed to scale to real-world programs. Affordable proof of ordinary software's global correctness is no longer a goal and certainly not a promise of contemporary software verification.
It's very much the goal for PLT. :)
In practice, it's also very much in the future. Right now verifying large programs is possible for a team of experts with a lot of time and money. A lot of the work in the 21st century has been to scale these theoretical methods to real languages. Most of the really big verification projects of today were unthinkable a decade ago. A decade or two in the future it'll probably be routine and just another tool you use, similar to static analysis or unit tests.
Right now the infrarstructure is just not there yet, and that's one of the reasons why formal verification is so expensive. But there are no fundamental restrictions which would prevent us from verifying, say, the Linux kernel. Apart from it being way too expensive. If it was written in a reasonable languages, which encouraged programmers to develop truly sound abstractions it could be orders of magnitude less expensive, though...
Maybe. Maybe not. No one knows for sure, and no one has anything to suggest that the path forward is now clear. Those results provide good enough cause to believe that the problem is very hard. Empirical experience only strengthens the belief in that assumption (suggesting that we cannot easily find an easy-to-categorize subset of programs that is generally useful yet easier enough than the worst-case).
> Here's one way to make termination proofs modular: Take the graph of your function (vertices for each value of the arguments, edges for recursive calls) and take its transitive closure. If you can cover the transitive closure with an arbitrary number of individually well-founded relations, the function terminates.
Sure, that's how abstract interpretation works. But it doesn't always work, and proving termination says absolutely nothing about proving other properties.
> Does the consistency of ZFC "elude the power of math"?
Yes.
> The point of having contextual equivalence or a program logic is that every property you can express in your programming language/logic survives this state reduction.
Then those properties are weak or the reduction is hard. It's a simple consequence of bounded halting and the model checking results (also, I think I've seen Cousot give some simple examples of properties that cannot survive state reduction). In any event, even if you find properties that you can reduce in this way, the "model-checking isn't FPT" result, shows that you won't be able to combine them to prove global results (unless the local property happens to be all that's necessary).
> Right now verifying large programs is possible for a team of experts with a lot of time and money.
No large or even mid-sized program has ever been verified using PLT methods, no matter the size of the team or the effort. A medium sized business program is ~1MLOC. A large one is ~5-10MLOC. Programs that have been formally verified using PLT approaches are hardly within an order of magnitude from 100kLOC (from below, of course). It is also important to know that those verified programs don't employ arbitrary common algorithms, but only the simplest possible algorithms, for the purpose of verification.
> It's very much the goal for PLT. :)
What gives you that impression? My impression is that the goal is to verify important "kernels" for security or other crucial properties, at some acceptable cost given the small size and the great importance. Maybe some people hope that affordable whole-program verification would one day be possible (this is not unique to the PLT approach), but I don't think that's the current goal.
> A decade or two in the future it'll probably be routine and just another tool you use, similar to static analysis or unit tests.
I am not aware of a single researcher who believes that, but I'd like to know who does.
> But there are no fundamental restrictions which would prevent us from verifying, say, the Linux kernel. Apart from it being way too expensive.
I'm not sure what you mean by "apart from it being too expensive". A restriction that sets the complexity of that task at more than the lifespan of the universe would be a fundamental restriction. Anyway, there are no known ones, no. But it's like saying that there are no known fundamental restrictions that prevent us from proving P /= NP or the Goldbach conjecture, but stating confidently that either will be accomplished in some known timeframe is a whole other matter.
> If it was written in a reasonable languages, which encouraged programmers to develop truly sound abstractions it could be orders of magnitude less expensive, though...
We don't know that at all, and there are certainly no known results that suggest this may be the case. No one knows whether "good abstractions" make verification scalable. This may be what some people hope, but it is no more or less promising, and no more or less substantiated than the hope that, say, CEGAR model checkers would be able to verify the Linux kernel. Both are theoretically possible outcomes, both show some promise, but neither makes us confident that it will one day be so. If anything, my money is on CEGAR, or some combined approach where CEGAR would do most of the work.
> Sure, that's how abstract interpretation works. But it doesn't always work, and proving termination says absolutely nothing about proving other properties.
Abstract interpretation has nothing to do with disjunctive well-foundedness. The latter is a specific proof method which has pretty much revolutionized automated termination proving in the early 21st century (due to being modular and therefore allowing for easy combination of decision procedures).
>> Does the consistency of ZFC "elude the power of math"?
> Yes.
Yet I can easily show ZFC consistent in CiC with excluded middle at Type. Sets are graphs modulo bisimilarity, choice follows from excluded middle at type. Conversely, classical CiC is consistent relative to ZFC with enough Grothendieck universes. Math doesn't end at ZFC, and no, not even in practice (higher category theory pretty much requires these constructions).
> I'm not sure what you mean by "apart from it being too expensive". But it's like saying that there are no known fundamental restrictions that prevent us from proving P /= NP or the Goldbach conjecture, but stating confidently that either will be accomplished in some known timeframe is a whole other matter.
One of them requires lots of perspiration, the other requires some fundamental new insight.
This is not science fiction. It's not even fiction. You can sit down right now and show the correctness of arbitrary data structures and algorithms in Coq, using, e.g., Charguéraud's CFML. You can even verify arbitrary C programs, using VST, even though I wouldn't recommend it (seeing what guarantees the C semantics really give you, compared to your mental model of C can lead to night terror in adults).
> Abstract interpretation has nothing to do with disjunctive well-foundedness.
Abstract interpretation has to do with every proof technique regarding computation.
> The latter is a specific proof method which has pretty much revolutionized automated termination proving in the early 21st century (due to being modular and therefore allowing for easy combination of decision procedures).
That's great, and model checking and abstract interpretation completely revolutionized many kinds of program proofs -- termination, temporal logic, memory safety and many more -- but the fact remains that no one has ever been able to fully verify a large real-world program using any known technique, and no one -- to the best of my knowledge -- seems to think we're on the path that will get us there any time soon.
You'll find that the people who use formal methods on a regular basis (like me, if only in the past year or so) are the ones that are most cautious about pie-in-the-sky promises. Yes, some things will get easier; yes some properties will become easy to prove. But full, affordable program verification? Probably not in the foreseeable future, if ever. People like Xavier Leroy, who are experts in deductive verification methods are always very cautious about making such optimistic promises. Leroy, e.g. believes that deductive methods are suitable only for smallish programs.
In fact, when it comes to manual formal verification, I am not aware of anyone who claims they will become generally affordable any time soon. Automated methods (model checkers and SMT solvers) are used almost exclusively for real-world programs, with only a small smattering of manual deduction, usually to tie together automated results. Right now, the goal for manual deduction is to match the cost of current high-assurance development (which is too expensive for ordinary programs, if possible at all, due to size). Manual deduction also seems especially sensitive to algorithm complexity (not computational complexity, but "conceptual" complexity, which may be related (perhaps to space complexity more than time complexity)), but really the potential effectiveness of various methods to affordable whole-program verification is no more than a personal affinity at this point. No one has anything definitive to claim.
What I do find interesting is that it is PLT fans (maybe not the researchers themselves who are usually more cautious) who make the most outlandish claims despite the fact that when it comes to verification, PLT has had less real-world success than pretty much any other approach. Perhaps it's because those techniques are least put to the test, so there are no disappointments.
> Yet I can easily show ZFC consistent in CiC with excluded middle at Type.
I don't understand. Then the same result applies to CoC. There is nothing intrinsically special about ZFC as a formal foundation, it's just what most people take as the foundation. If you want to base math on another foundation go ahead, but an unprovable program exists in whatever foundation suits your taste, too.
> One of them requires lots of perspiration, the other requires some fundamental new insight.
You've just thrown all of complexity theory out the window. "Lots of perspiration" can mean (provably!) more resources than the entire universe can afford. Theoretically winning at Go also required little insight; actually winning required a lot of insight (namely, restricting the problem to facing human opponents and studying their behavior). If anything, it is the difference between decidability and undecidability that is of lesser importance than difference in "perspiration".
> Abstract interpretation has to do with every proof technique regarding computation.
Are we talking about the same thing? Abstract interpretation as formulated by Cousot consisting of a covariant galois connection between a particular kind of denotational semantics (collecting semantics) and a complete lattice with finite height or well-founded widening/narrowing functions. It's not the final word in program logics by a long shot. For example, collecting semantics is lossy for reactive systems and ... I'm not even sure what the story with concurrency is. I know that Cousot and others extended it to higher order languages at some point, but this is not mainstream as far as I know.
> I don't understand. Then the same result applies to CiC. There is nothing intrinsically special about ZFC as a formal foundation, it's just what most people take as the foundation. Whichever foundation you choose, an unprovable program exists.
Yes, and this is the true point of Goedel's proof and the (partial) failure of Hilbert's program. In this case you cannot have your pie and eat it too. You can't quote Hilbert to claim that ZFC is the accepted foundation of mathematics and then quote Goedel to say that this doesn't work. Goedel's results are not just making a statement about programs, they demonstrate the failure of mathematical realism, and even Goedel himself never quite got over it.
> You've just thrown all of complexity theory out the window. "Lots of perspiration" can mean more resources than the universe can afford.
I didn't even consider that you believed this to be the problem. The thing you have to understand is that there are not that many PLT researchers. The group around Xavier who are responsible for CompCert conists of a handful of people and most of the work was done in < 5 years. Most startups in SV are better funded and staffed than pretty much every formal verification project. CompCert with a single backend (there are 3 official backends, with several ABI targets each) has about 60 kloc of ML code when extracted and about 100 kloc more in Coq proofs, the factor between code and proof you are looking at is about 1:2.
Most importantly, and unlike model checking or other completely automatic approaches, this is apparently a constant factor. So a good approximation is that you would have to write a program which is twice as large as the linux kernel (~20 mloc) plus the related tooling. This is certainly a big project, but I'm positive that we can meet your deadline of "before the heat death of the universe".
The thing that I find troubling -- in spite of following and enjoying the progress in program verification -- is that in every other scientific-professional discipline, like medicine, researchers always caution about misrepresenting results (this drug looks promising, it works on mice, and it may hold promise for humans; they get annoyed when the media is overly optimistic) and virtually all practitioners are even more skeptical than the researchers. In CS/software, people make some progress in verifying a specific property of a specific lab-sized program, and many practitioners declare "halting problem solved!" (I'm exaggerating, but that's the gist). I get the feeling that a few researchers tacitly encourage this state of affairs. I see this in PLT more than in any other subdiscipline of CS (along with -- maybe -- machine-learning).
There is constant progress on many fronts, and it's perfectly OK to get excited, but hyped overpromising has led to significant setbacks in CS in the past (including in formal methods in particular) because the greater the hype the greater the disappointment. We should be happy with what we have without claiming (falsely) that all of our problems are solved. If anything, cautiously downplaying research results is a much better strategy to long-term success.
I think there are different discussion forums for different things. Right here, I'm talking to you because I'm interested in hearing your point of view and perspective, and I want to know how you react to mine.
In a professional context it is expected to downplay results and to be very cautious. Research is an expensive and volatile investment at the best of times, and overstating your success to secure funding could easily lead us into the next AI winter... So if we were to meet at a conference, I would still hold the same views, but I would never express them in a talk or in any other official capacity.
If you see researchers overpromising results, e.g., in the contributions section of a paper, then that is very bad form.
I think healthy skepticism is no less important in professional settings than in academic settings. I don't think pharmaceutical researchers oversell research drugs to physicians (although drug salesmen certainly do), and if they do, it's just as bad, and I hope doctors are skeptical.
> Abstract interpretation as formulated by Cousot consisting of ...
Abstract interpretation is the general theory of Galois connections on program representations be they syntactic or abstract Kripke structures. Any sound abstraction (i.e. reduction) of the state space -- syntactic or semantic -- that preserves logical properties for the sake of verification is basically abstract interpretation. Widening/narrowing are just techniques to create sound reductions through fixpoints; I don't think they're essential to the concept of abstract interpretation (Cousot calls model checking, type systems and deductive proofs special cases of abstract interpretation).
> You can't quote Hilbert to claim that ZFC is the accepted foundation of mathematics and then quote Goedel to say that this doesn't work.
I didn't "claim" that ZFC is the accepted foundation. It is the normally assumed foundation so I picked it, but the choice is irrelevant.
> Most startups in SV are better funded and staffed than pretty much every formal verification project.
And need to build far bigger things.
> this is apparently a constant factor.
I would be extremely careful saying that. It is a constant factor when extreme care is taken to keep algorithms "braindead simple" (as someone who'd worked on seL4 once called it) and when the program size is kept to somewhere between tiny and small.
> but I'm positive that we can meet your deadline of "before the heat death of the universe".
Yes, obviously. The problem with all formal methods, though, is that the deadline isn't the end of the universe, but something that is considered affordable. My personal issue with manual deduction in general (I have more particular concerns with some PLT approaches) is that the approach is less amenable to approximate verification. In other words, making full-program end-to-end verification cheaper would not affect most software as it would still be too high a price (at least for the foreseeable future) to pay for something most software doesn't need. A bigger impact would be to reduce the cost of gaining the currently (or somewhat better) attainable level of confidence.
> Cousot calls model checking, type systems and deductive proofs special cases of abstract interpretation
Maybe he said something like "[...] can all be seen as abstract interpretations". But it's probably not always useful to do so.
Abstract interpretation has been enormously successful, not least because it is modular: there are standard ways of combining abstract domains. This is a huge advantage, especially compared to ad-hoc techniques in program verification, but it depends on your abstractions being connected to the same kind of semantics.
In particular, disjunctive termination proofs can be shown to be sound through Ramsey's theorem, and I don't see how to formulate this as an adjunction at all. Even if it is theoretically possible, the statement is a bit like saying that "all programming languages are equivalent to Turing machines". Even if that is true in principle, you wouldn't want to develop your next product as a big string rewriting system...
> I didn't "claim" that ZFC is the accepted foundation.
The point is, that these questions are not "beyond the power of math". Mathematics is like an amorphous blob, which expands as needed to encompass new and interesting problems.
If there was an interesting problem which was provably independent of ZFC, people wouldn't just give up. They would try to look for "natural" or "intuitive" extensions in which the problem can be "settled". Case in point, the continuum hypothesis is independent of ZFC, and so people developed extensions where the answer could be settled either way. Goedel himself was convinced that this is a question which could be "answered" by identifying which of the proposed extensions is more "natural".
You don't have to look to programs to find questions which are apparently "beyond math". Any kind of self-referential statement gives you such a question. Programs are not special in this regard, you could always do the same thing in logic.
> I would be extremely careful saying that. It is a constant factor when extreme care is taken to keep algorithms "braindead simple" (as someone who'd worked on seL4 once called it) and when the program size is kept to somewhere between tiny and small.
This is mostly a question of economics. In research, you have tight time constraints and comparatively little man power. You can take current data structures for weak memory concurrency and verify them end to end, but if the goal of your project is "building a verified C compiler", then this is not a good use of your time.
In truth, big research projects are just as conservative as big companies, if not more so. The architecture of CompCert (as originally implemented) is at a level you would find in an 80s handbook on compiler construction. This is not because Xavier doesn't know better (see OCaml), it's because they absolutely couldn't afford for the project to fail, or even to be delayed.
In my experience, complex data structures and algorithms aren't actually that much more complicated to verify than simple ones. The main work is always in finding the right specifications, and modelling the problem in your proof assistant. For instance, if you have to verify a max-flow solver, then you will need to formalize graphs, flows on graphs, and duality. This is for writing down the specification (what is a maximum flow) and showing that it has the right properties (e.g., is unique). Once you have all of this machinery, the final correctness proof of, say, the Edmonds-Karp algorithm is not a lot of work (see https://www21.in.tum.de/~lammich/pub/itp2016_edka.pdf). Based on this background theory, it would also not be particularly difficult to verify some variant of Preflow-Push.
But again, if you have a concrete problem you want to solve through max-flow, then you would be done once you have verified the abstract augmenting paths algorithm. Heck, in this case you would probably just verify a validator and implement the solver in untrusted (but memory safe) code.
You know, seL4 is actually a good example of economic pressure on research projects. I don't know how to say this nicely, but the correctness proofs of seL4 are extremely ugly. There just wasn't enough time to look for elegant specifications or proofs, or to reformulate algorithms and data structures to make the proofs nicer. That's not to say that it cannot be done. It's certainly one goal of the CertiKOS project to build better tools for OS verification.
> Yes, obviously. The problem with all formal methods, though, is that the deadline isn't the end of the universe
Look, your argument was that the state space is exponential in the program size, therefore verification takes exponential time since it is fundamentally impossible to build modular correctness proofs. All I'm saying is that based on the empirical evidence, this is false. There are plenty of modular proof techniques and all formal verification projects (in the ITP sector) that I'm aware of report the overhead of verification as a constant factor.
> My personal issue with manual deduction in general (I have more particular concerns with some PLT approaches) is that the approach is less amenable to approximate verification. In other words, making full-program end-to-end verification cheaper would not affect most software as it would still be too high a price (at least for the foreseeable future) to pay for something most software doesn't need.
I completely agree with you on the last part, but what makes you think that we can't drop down the level of assurance for parts of the program? Chlipala's Bedrock project built a verified web server in Coq. The lowest levels of this (the implementation of threading, data structures, memory allocation, tcp stack, etc) verify full functional correctness, while for the higher levels (user interface, etc), they merely show the absense of run time errors.
This seems like a sweet spot for most applications. You can verify full functional correctness for library code, or core OS components, while applications are merely free of memory errors or other bugs which could crash your program. How much money would you save in the long run if you knew for certain that the infrarstructure that is running your software cannot break?
---
Personally, I think that the most promising application in the near future is actually just better documentation. If people were more aware of formal methods and would specify precisely what a certain function ought to do, we would probably eliminate a lot of bugs right there. I'd also expect that thinking more deeply about your programs should lead to better architectural decisions and better abstractions. But this doesn't work if you force people to use first-order logic, with some limited set of temporal operators. You need a language which is at least as expressive as the natural language specifications that people are already using. This is why I focus so much on program logics and PLT methods.
> In particular, disjunctive termination proofs can be shown to be sound through Ramsey's theorem, and I don't see how to formulate this as an adjunction at all.
I have no idea what you just said, but I believe you :)
> it depends on your abstractions being connected to the same kind of semantics.
I'm side-tracking, but "semantics" requires a language. Not all computations are expressed in a language, and AI applies even to those of them that are not.
> If there was an interesting problem which was provably independent of ZFC, people wouldn't just give up.
Again, this is not the point. Whatever logic you choose, there would be programs whose behavior you cannot predict.
> You don't have to look to programs to find questions which are apparently "beyond math".
Of course, but we're talking about programs, and no one can deny the role of programs in the history of mathematics as examples of things that are hard (or impossible) to reason about.
> All I'm saying is that based on the empirical evidence, this is false. There are plenty of modular proof techniques and all formal verification projects (in the ITP sector) that I'm aware of report the overhead of verification as a constant factor.
This is indeed the main point of debate, although I'm not insisting on "exponential". The theory says things can in be really expensive (exponential and more), and the question is whether real-world programs are contained in a subset that is entirely different -- easy to verify -- or that they are spread throughout and can turn out to be arbitrarily hard (close to the worst case). I don't think empirical evidence settles this question, and it certainly doesn't suggest real programs are easy to verify. It is also certainly true that some programs -- when kept small and very simple -- in some specific domains, under lab conditions, have turned out to be not so terrible to verify. As someone who practices formal methods almost every day, I will certainly not say that things are hopeless, but I don't think we're in a position to say that the solution is near. We really don't know enough.
As someone who uses formal methods to reason about very complex distributed and concurrent algorithms (although deductive proof would take far more resources and time than we can hope to spend), formal verification works well (although I and many others who do this in the industry are skeptical about deduction), but the problem is different from program verification.
> This seems like a sweet spot for most applications.
Oh, I have no argument with you there. I totally agree. Deductive methods for the small, sensitive core if automated methods don't work, and automated methods -- with various degrees of confidence -- for the rest. But this isn't the same as saying that PLT approaches have "solved verification".
> This is why I focus so much on program logics and PLT methods.
Have you given TLA+ a look? I think it covers exactly what you're looking for far better than any PLT solution I've ever seen, for many reasons (generality, simplicity, ease, tooling, elegance). I'm always amused when I see yet another academic paper about formulating something in Coq, that an "ordinary" engineer would do with no more than little thought within a month of first laying eyes on TLA+. Just today I watched this talk from ICFP: https://www.youtube.com/watch?v=caSOTjr1z18 It didn't really make me understand what HoTT is about, but it did make me realize that PLT has taken a wrong turn somewhere and seems to be falling into the rabbit hole of foundational logic, if so much thought is put into a "computation" that isn't even algorithmic (i.e., it has a computational complexity of 0, and serves not the program but the formalism). If I remember correctly, "older" typed languages that PLT people are fond of like SML, didn't even have this problem that now requires a new foundation for mathematics (I'm exaggerating, but I think that not by much).
------
This, BTW, is a Twitter conversation between PLT-verification people, one of whom has worked on seL4. The bottom line is that we should work on FM -- it works in many cases -- but certainly "dismiss illusions" about it:
What's the definition of an informal proof, and in what sense can it be exponentially smaller than a formal proof? Even if you can answer this, it sounds as if you are ignoring all the progress we have made in programming language design. The whole reason we have modern programming languages is to bridge the gap between the "informal proof" you keep in your head and an actual formal correctness proof.
For example, C programs typically have a lot of bugs because there is such a large disconnect between the model of the program in your head (which also lacks most of the error states) and the actual state space of the program. Almost every abstraction in C is potentially leaky, and this just doesn't allow you to reason succinctly about your program. This is not even specific to C. The "simple" imperative programming models that are still used almost everywhere have exactly the same problem.
The point of modern programming languages isn't that it's essentially the same thing, but with a scalable static analysis tacked on (types). The point is that we try to impose a discipline on programs which allows for modular correctness proofs. If you have a module implementing a certain data structure in ML, you can reason by parametricity about its correctness and once you have established whatever properties you want, nothing will every break them again. Essentially, you have just taken part of the state space and shrunk it down to a single bit.
And that this is possible is not at all surprising! Everything you write, here or in your article, is also applicable to ordinary mathematics. So if theorem proving is fundamentally difficult, how do we make progress in mathematics? By finding new abstractions and by composing abstractions.
We are making real progress in verification. Nowadays, there are scalable proof techniques for concurrent programs, even in the presence of weak memory models (GPS, iCAP, Iris, ...). There are compositional proof methods for program equivalence which scale to real programming languages (step-indexed logical relations, ...). There are language primitives for safe, efficient and easy to reason about concurrent and distributed programming (e.g., join calculus). And many, many more things which were previously thought of as stupendously complicated.