Total Functional Programming [pdf]
citeseerx.ist.psu.edu
citeseerx.ist.psu.edu
A program in Haskell can only crash in one way (on a hypothetical computer that doesn't break or run out of RAM): if you write a function that doesn't have an output for every input. You can prevent this through totality checkers such as the one presented in "GADTs meet their match", which you can enable in GHC, the most popular Haskell compiler.
However, programs can still loop forever.
There are several approaches to fix this. One approach is to require recursive functions to monotonically decrease on their arguments. Languages like Idris and Agda support this. The downside is you are no longer Turing complete.
The approach mentioned in the paper is to make a formal distinction between finite and infinite data (data and codata), and in this way you can keep termination checking for functions on finite data, but you also get to keep Turing completeness. What you do instead of proving completeness for functions that might run forever is you prove that the function "does something useful" every time it recurses.
If not, your program could be "total" in most of the useful senses, and subparts could have tighter bounds, without any harm.
Also, I recommend reading Harper's throughts about it:
"Old Neglected Theorems Are Still Theorems" https://existentialtype.wordpress.com/2014/03/20/old-neglect...
It also reminds me of the NASA coding standards, rule 4:
"All loops must have a fixed upper-bound", see http://pixelscommander.com/en/javascript/nasa-coding-standar...
(Related HN discussion: https://news.ycombinator.com/item?id=8856226)
A tactic language doesn't need to be total, since it's only run at compile-time, so no errors can leak into the resulting proof/program. The worst that can happen is the compiler hangs.
Coq comes with "ltac", which is a horrible imperative language that leads to very fragile proofs. On the other hand, mtac is just Coq's normal, total FP language ("gallina"). A monad is used to wrap up general recursion, so that gallina can be used un-changed.
During compilation, these monadic values are forced, which either leads to a value or causes the compiler to hang. This is a really nice compromise, since you can write Haskell-style FP code which "obviously terminates", without having to prove that it terminates, you still have access to all of the nice dependent type machinery, and the end result (the program, not the meta-program) is guaranteed to be total (unlike, say, an Idris function which turns off the totality checker).
What are you referring to? Data/codata checking works with local type inference.
Huh?
inf = Cons 1 inf> Each recursive function call must be on a syntactic subcomponent of its formal parameter.
But it doesn't. But you can't actually use that to get a nonterminating program, because you can't recurse over it:
> Ordinary recursion is not legal over codata, because it might not terminate.
This is similar to the Brown-Palsberg self-interpreter in a total language, which caused a lot of confusion recently because it's not a self-interpreter (it doesn't take source code as an argument). I think it's better to stick with common definitions and accept that total languages are not Turing complete and can't self-interpret.
Is it a common error? Who's commonly saying this? Can you link any examples? It seems a really strange claim to make.
There are a couple in this very discussion:
https://news.ycombinator.com/item?id=12648261
https://news.ycombinator.com/item?id=12648932
A quick Google search I did just now came up with this one, by someone who knows better[1]: By writing programs in a total language like this, you can confidently answer questions that you can't with a Turing-complete language. You've overcome theoretical limitations by changing the problem parameters a little bit—a common approach in engineering.
The only question you can confidently answer is "does the program halt", to which the answer is always yes. You cannot confidently answer any other question any easier than in non-total languages.
You can find more examples in recent discussions about the Ethereum heist, with many suggestions to "just use a non-Turing complete language". Many seem to believe that there are languages that make verification easy, or that Turing completeness is the problem.
> It seems a really strange claim to make
I guess the reasoning goes like this: the impossibility of proving things in general about programs is a result of the halting theorem; we can get around the halting theorem by using languages that only admit programs that halt; assuming the language is still useful -- problem solved!
How many people know about bounded halting? I know I hadn't until rather recently, when I thought about it and somebody pointed out to me that it's at the very core of the time-hierarchy theorem. I think I actually thought about it because of total languages, when I realized that every program can be assumed to be total without loss of generality, and so totality cannot add actionable information.
[1]: https://www.quora.com/Can-we-solve-the-halting-problem-by-de...
Free (() ->) Integer
The actual definition of Turing completeness is the ability to implement any program that a Turing machine can compute, which you can with corecursion.
http://docs.idris-lang.org/en/latest/tutorial/theorems.html#...
The topic often comes up in the discussion of smart contracts on public blockchains, and people often get confused about what Rice's theorem says. I recently did a small write up on the topic (plug, plug)
https://hackernoon.com/smart-contracts-turing-completeness-r...
In your post, you write:
> However, almost all correct programs of interest are going to be essentially provably correct. Moreover, the proof of their correctness will be relatively straightforward.
This has been shown to be false in practice. The difficulty of proving real-world program correctness shows that real-world cases can get arbitrarily close to the worst-case predicted by the theory. Proving small programs like seL4 took required experts, and even then demanded an extreme simplification of all involved algorithms so that proof would be feasible. Even then, the cost was far beyond what any "ordinary" software could afford, and even after a great streamlining of the process and the use of "easily verifiable" languages, it is expected to be suitable only for resource-rich high-assurance software.
Note that I'm not saying that formal methods are useless. I regularly use formal methods myself. But making them affordable is an art.
I've written at length about the relevant theory here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
1) Yes, even in weak models, proving correctness is still intractable in general. However, this does not mean that a general algorithm has to be slow when run on typical instances. Typical instances are designed with a proof of correctness in mind, which is a strong indication that such a proof should be accessible.
Unless you're generating programs randomy, programming generally entails carrying at least an informal proof of correctness in mind.
2) As you point out it is currently very hard and tedious to formalize those proofs. However, I believe this isn't a fundamental barrier. We need better tooling, more clever proof-finding algorithm to bridge the gaps, clearer interfaces. Importantly, it is not a computational barrier.
There is nothing about the formal verification of typical software that intrinsically requires expensive computations. Compare it to image recognition. It used to be very hard to do in software and it didn't work well. But when it finally started working, it didn't turn out to be particularly computer intensive.
I think the same is true in formal verification. We don't know how to do it very well, but we're not up against theorems in complexity theory, we just lack the know-how.
True, but we have a few decades of experience with model checkers running on real programs. Yes, they work very well and are quite affordable, but their domain is rather specific (there is amazing work on model checkers designed to expand their domain and work on ever-larger programs, but the results aren't in yet).
> Unless you're generating programs randomly, programming generally entails carrying at least an informal proof of correctness in mind.
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.
> We need better tooling, more clever proof-finding algorithm to bridge the gaps, clearer interfaces.
Absolutely, but we must understand there are fundamental problems in play.
> Importantly, it is not a computational barrier. There is nothing about the formal verification of typical software that intrinsically requires expensive computation.
This is unknown, but not very promising; certainly not promising enough to assume this will definitely be possible some day (let alone soon). See the result about symbolic model checking (basically the cost of proof that is allowed to exploit linguistic constructs) that I mention in my post. It turns out that in the general case (this time, we're not talking about completely "random" programs, but "random" programs that can be expressed succinctly in some language), it is as hard as a proof that doesn't exploit language, and the difficulty was found to hold in practice (the paper I quote calls it an "empirical fact"), i.e., real-world programs do get close to the worst-case.
The goal of software verification nowadays isn't to find methods to verify general programs, but to find methods that catch a particular class of bugs (static analysis) or to prove arbitrary properties for specific domains or small programs (model checkers). The PLT approaches mostly focus on end-to-end verification, and don't currently attempt to make it affordable for "ordinary" programs. They're trying to make it as affordable as high-assurance testing (the kind done at NASA). In the seventies, the hope was that formal methods would one day allow us to prove arbitrary correctness properties of ordinary software. This is no longer the goal of the verification community today, despite the great achievements in some areas.
[1]: Even when the informal proof is not just "in mind", but on paper, written by experts and peer reviewed: https://brooker.co.za/blog/2014/03/08/model-checking.html
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.
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.
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.
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 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".
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.
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.
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.
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.
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:
https://twitter.com/jonsterling/status/755794232929955840
I have an idea… We should ban the use of the word “trust” in “program verification” / “formal methods” circles.
https://twitter.com/jonsterling/status/755794326123196416
Well, if you ask me, we should ban the entire field of “formal methods”. Such a complete waste of time! very sad.
https://twitter.com/jonsterling/status/755794588300812288
By “waste of time”, I mean it’s intractable and really gnarly. Lot of folks get interested in it b/c they like type systems, but anyone who
https://twitter.com/jonsterling/status/755794781511389184
…is serious in the field knows that beautiful type theories aren’t going to get it done. What’s needed there is pure muscle and endurance
https://twitter.com/jonsterling/status/755794833437036544
…to bang through millions of lines of incredibly gnarly isabelle or coq code.
https://twitter.com/kamatsu8/status/755795189172539392
@jonsterling True. On my more cynical days, I say the main contribution of our seL4 project is the effective use of cheap student labor.
https://twitter.com/jonsterling/status/755795291949760513
@kamatsu8 Sorry, btw, for being snarky and dismissive. I should not have said “ban” but rather “dismiss our illusions about”.
https://twitter.com/kamatsu8/status/755798589075361792
@copumpkin @jonsterling In general I'd say formal methods are probably worth investigating, but there isn't going to be a silver bullet that
https://twitter.com/kamatsu8/status/755798808232026113
@copumpkin @jonsterling makes it always worth doing, which many FM people pretend exists even though it's provably impossible
https://twitter.com/kamatsu8/status/755798899319726080
@copumpkin @jonsterling and it's always going to be at least a little bit unpleasant.
[0] Specifically the generic case decidability of the Halting Problem for one-sided tape Turing Machines? https://en.wikipedia.org/wiki/Generic-case_complexity#The_ha...
As to whether the class of programs humans write are theoretically feasibly verifiable, nobody knows for sure, but the problem is certainly not easy, judging by all attempts so far.
My favourite point was that simply by adding an instruction counter, we can make every program terminate, but this does not make the program considerably easier to reason about. It reminds me of Ethereum's limit on Turing Completeness (Gas).
So the idea seems to be a programming framework that on one hand guarantees termination, while on the other hand is sufficiently powerful to be useful. That is "useful despite being sub-turing".
I spent some time causally studying the subject of sub-turing languages, and found something notable. If a language guarantees that all its programs consume input as they go, that program is guaranteed to terminate, and so the language itself is sub-turing. One example of such program could be a compiler, which makes for a great example of a useful application of a sub-turing language.
It's a fascinating subject because sub-turing language programs are a lot easier to analyze.
link(codegen(analyze(typecheck(parse(lex(source))))))
This has been called being "Pacman Complete" by Edwin Brady. I very nice catchy term, IMO.
The paper opens with:
The driving idea of functional programming is to make programming more closely related to mathematics.
From a paper by John Backus:
Associated with the functional style of programming is an algebra of programs whose variables range over programs and whose operations are combining forms. This algebra can be used to transform programs and to solve equations whose “unknowns” are programs in much the same way one transforms equations in high school algebra.
Are they talking about the same thing here?
Also, are there advantages to having such an algebra of programs outside of correctness verification?
Yes, they're talking about roughly the same thing. The kernel of the idea is called "equational reasoning", which exploits the key mathematical characteristic of functional programs, that they are referentially transparent [0].
> Also, are there advantages to having such an algebra of programs outside of correctness verification?
Proving correctness is a big one, but you can also use these techniques to derive more sophisticated algorithms from a naive (but correct) first implementation. For an example, see section 4 on the implementation of an efficient minimax algorithm in a short paper by Richard Bird [1]. (You will have to read some of the previous sections to understand the example.)
If that piques your interest, Bird's introductory book on functional programming written with Philip Wadler [2] introduces the technique, which is usually called "program calculation". (Though published in 1988, their book remains a great introduction to functional programming.) If you really want to go off the deep end, Jeremy Gibbons's extensive lectures notes, published as a book chapter [3], are the best source I know. (Beware: here be category theory.)
0. https://en.m.wikipedia.org/wiki/Referential_transparency
1. R. Bird (1988), "Algebraic identities for program calculation", http://comjnl.oxfordjournals.org/content/32/2/122.full.pdf [PDF]
2. R. Bird and P. Wadler (1988), Introduction to Functional Programming. It's out of print and hard copies are scarce, but a scan is available at https://usi-pl.github.io/lc/sp-2015/doc/Bird_Wadler.%20Intro... [PDF]
3. J. Gibbons (2002), "Calculating Functional Programs, http://www.cs.ox.ac.uk/jeremy.gibbons/publications/acmmpc-ca... [PDF]
Totality does in no way make proving correctness easier in practice. See http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
Totality really mostly helps when using typed programming languages as proofs of general (non-executable) mathematical theorems via propositions-as-types. Without it, the logic will be inconsistent. For actual programs, though, it makes little difference.
It's not just that "there is more", it's that there is everything.
The halting problem which we're talking about here is actually easily generalizable into a set of generic theorems about static analysis of programs in general. The usual first step is to prove the first incompleteness theorem (no axiom system proves all of the interesting facts about the integers), then modify that into a proof of the second incompleteness theorem (that every logic which proves its own consistency must be inconsistent). But it goes way further than that to Rice's theorem: every nontrivial semantic property of a computer program is undecidable. Put another way, the only way for the compiler to know that something is true is for there to be a really simple up-front convention which makes it true.
Suppose you want to make sure, statically, that you never dereference a null pointer. This says that the only way a compiler could ever be strong enough to prove this is if it's syntactically impossible to create a null pointer in the language in the first place, so that it's a "trivial property" of all programs that they never dereference null pointers.
Suppose you want to prove that a certain block of code is the fastest possible code which does a certain thing. The only ways to do this require the language to "normalize" all of its expressions so that there is only one block of code for everything you want to do. If there's more than one way to do it, then the analysis "is this the fastest code?" is nontrivial and you can't prove it! (You can always get heuristics of course to try to cover the most common cases, but your heuristics will never cover everything you want.)
Suppose Microsoft wants to fix Word and Excel's macro systems to a new form that cannot contain viruses: the only way to do that is if the macro system is either (a) Turing-incomplete, so that you can analyze its programs, or else (b) unable to do the virusy things that you're worried about in the first place. Otherwise there will always be a macro-virus which passes the virus-checker.
No, no, no. The original halting theorem is avoided in total languages, but the much more important version which forms the core of the time-hierarchy theorem, sometimes known as "bounded halting", holds unchanged. It is a generalization of halting which basically says that you cannot know anything about a program (including halting) any faster than running it (more precisely, you cannot know whether a program P halts in input x within n steps in fewer than n steps; all the other corollaries like Rice follow in the same way). This means that the cost of verification is the same for total and non-total programs, with the theoretically interesting but pragmatically irrelevant promise that the cost is some unbounded finite number in the total case.
If you want to convince yourself that totality cannot make proving program properties easier with an intuitive argument, consider this: take any program ever written, and to every loop and every recursive call add a counter initialized to 2^100 that is decremented with every iteration/recursion and stops the program when it reaches zero (which will not happen until the end of the universe). Your program is now provably total, yet its semantics have not changed a bit. I.e., you can already assume without loss of generality that every program is a total program and that every language is a total language. Is verification easier now that you know this?
The only case where you cannot make this assumption is when your language is used as a theorem prover to prove general mathematical theorems (that aren't executed and may actually "reach" infinity), and this is where totality matters.
See my post for a more in-depth discussion: http://blog.paralleluniverse.co/2016/07/23/correctness-and-c...
And we usually don't wait that long. A function that executes when loading a web page times out in the order of seconds.
Once you have deadlines, all bets are off - the function is not deterministic for any large enough input. Equational reasoning does not preserve performance - it could cause a program that previously ran fast enough to time out.
So, knowing that function terminates seems only theoretically useful. It doesn't tell us whether a program change is really safe. It would be more useful to put some kind of bound on the resources a function can consume.
In Etherium's language, there is a concept of "gas" which is an abstract limit on how much work a function can do. (The advantage over a timeout is that it's not machine-specific.) I sometimes wonder if anyone has applied this concept to functional programming? Could we define a language so that it uses static analysis to maintain guarantees about a function's use of gas?
Have a look at areas like "cost semantics", e.g. http://lambda-the-ultimate.org/node/5021
This takes a language's semantics, i.e. how to evaluate each sort of expression, and extends it to include extra information which can represent time taken, memory usage, cache usage, etc.
A simplistic way to track big-O complexity in types is given at http://twanvl.nl/blog/agda/sorting
Note that "gas" systems don't need to produce their result within the given gas limit; it's acceptable for the gas to run out and no value to be produced. This is trivial to prove correct, as it only requires that the language/DSL correctly keeps track of the gas, which can be done "once and for all" since it doesn't have anything to do with whatever algorithm you're writing to use the gas.
The machinery for doing that is old hat to functional programming: tracking gas usage is basically a Writer; stopping when gas runs out is basically a Maybe.
Statically ensuring that a function is within a gas limit is like statically ensuring that a "Maybe t" value contains a "t" value (as opposed to "Nothing").
This simply says that functional languages could be assigned cost semantics, just like imperative languages have, and so may be used for algorithm analysis. It has nothing to do with verification.
> tracking gas
Yep, but that's a trivial property that could be done by any runtime. It doesn't help prove any other correctness property.
fib (n+2) = fib (n+1) + fib (n+2)
There are also essentially no total languages today. Idris, Coq, etc. have support for totality, but there's nothing widespread or simple that does. I expect a total language would be quite useful in certain contexts (real-time, scripting, running user code, compilers), but the drive for - I can do whatever I want in this language - is so strong that a total language would need to provide significant, useful advantages to see adoption.
1. Totality doesn't guarantee that your program would actually terminate. A program that loops 2^100 times never terminates, yet is provably total. It is possible that empirically programs that are proven total turn out more likely to terminate, but in that case there is no need to enforce totality everywhere. You can prove termination whenever you like.
2. Proving totality can be extremely hard (yet another reason not to enforce it everywhere). So much so that Xavier Leroy, the world-expert who wrote CompCert, the only real-world, non-trivial program ever written in Coq, found termination proofs so difficult that he skipped them in CompCert, instead inserting a counter that he thought would suffice and throwing a runtime exception if it ever runs out before the function terminates.
As to total programming languages, safety-critical real-time software sometimes makes use of languages that are finite-state-machines, a far more restrictive model than Turner's total language. Nevertheless, bear in mind that even for FSMs, program verification is not generally tractable. How easy it is to verify a program depends almost entirely on one thing: how simple your algorithm is. All sorts of linguistic restrictions or safe runtimes can help prevent very important classes of bugs (like memory safety) that are local program properties, but do very little to make the cost of more global, logical properties affordable (which isn't surprising given that even the most restrictive computation model, the FSM, doesn't yield generally feasible verification).
As you obviously meant, no total general-purpose languages. I'm sure that HTML is total, for example. You also later qualified that "no total languages" meant "no widespread, simple, total languages", which I think is a very different statement!
It seems to me that your next sentence addresses this better than I could.
> that's not very interesting from the standpoint of totality: we already know that Web browsers are supposed to show something no matter how mangled their input is.
So isn't it interesting that they do that? I think that the prevalence of scripting languages on the modern web (and, if you like to look farther back in history, the reluctant Turing completeness of TeX) strongly suggests that it wasn't at all inevitable that we would get a total language for web design.
That is, to prove that it is total is presumably not much of an accomplishment, but that it is total is very interesting (and, from the point of view of the success of the web, important) indeed.
Edit: As far as HTML goes, I was attempting to describe "programming languages" - or perhaps algorithmic languages - which I don't consider HTML falling under.
For example, something as simple as assigning a variable has so much more meaning and functionality than I am used to, thanks to pattern matching.
I look forward to diving deeper into functional programming. Thanks for posting.
Functional programming tends to take this even further, by eliminating variable assignment to some degree or another. Different languages approach this differently, for instance:
- Erlang (and I assume this extends to Elixir) asserts a variable's value, rather than assigning it. You can see how this works by attempting to assign another value to the same variable: it will throw an error.
- Clojure (and I assume most lisps?) bind a variable to a symbol, but that only applies to the code that follows; if you access a binding, then rebind it, the previous access will only reference the original value. (Clojure, being impure, has ways around this in a bunch of ways.)
Once I grokked FP, I started thinking about this the other way around. If I see code like this in FP:
x = 5;
foo
In contrast, I read the same 2 lines in an imperative program as "first update the contents of memory location 'x' to contain '5', then evaluate 'foo'". This is much more complicated (i.e. has more meaning/function) than the FP version:
- We're specifying an evaluation order (do this, then do that), whilst the FP version works with any evaluation order. Among other things, this makes it difficult to evaluate in parallel (imagine if '5' were 'someExpensiveCalculation' and 'foo' were 'anotherExpensiveCalculationWhichMightNotUseTheFirst').
- We need a notion of "memory cells", which don't follow the lexical/syntactic nature of scoped variables; i.e. the first line may affect references in a seemingly separate piece of code. This makes reasoning much harder (although techniques like separation logic can make many common cases easier).
- The 'foo' calculation may affect the contents of 'x', so we can't trust the "equation" 'x = 5' to hold after (or even part-way-through!) the evaluation of 'foo'
One nice approach is "static single assignment"; it looks imperative (e.g. "single assignment C" looks like C), but it follows the FP semantics. In other words, it's useful when you want to show that your code is "straightforward": if you write it in C, the maintainer/compiler might guess that it's straightforward (e.g. that you don't invalidate the "x = 5") but doesn't know; in single assignment C, they know because the compiler enforces it.
https://en.wikipedia.org/wiki/Charity_(programming_language)
Very interesting stuff.