I get that we have mouths, vocal chords, lungs, brains, etc. It simply shocks me that some fellow humans use them to ridicule those things.. Once machines start making fun of us as they heal themselves (something we can do too.. go Life), I believe I'll get their humor, or what have you. I wonder if with their "big brains" some of them will still feel so inclined to speak unkindly about Earth's chemicals and processes that their bodies use.
That's an extremely narrow view of life. A broader view might be that life on Earth began a few billion years ago, and has managed to hang on ever since. Do you realize that you are, most likely, the direct descendant of one of those early lifeforms? Every single one of your ancestors, for billions of years, has managed to produce viable offspring in an unimaginably long chain of living organisms. How can you call that unreliable? Sure, bits of your DNA are being corrupted every second. Sure, tens of billions of your human cells die and are cast away each day. And, sure, each agglomeration of cells we call a human only lasts a few tens of years. But life has enough redundancies, contingency plans, and diversity that it will in all likelihood keep going for a long, long time.
Having a single instance of a particular organism last for a long time just isn't what life is about. If you look at the full context of what life is doing, it is way goddamn more reliable than anything humans have designed, proofs or not.
I agree with your argument as far as it goes, but if you're responding to me, you're making a straw man argument. I was saying that living things (i.e. individual organisms) aren't very reliable; you're saying that life is very resilient. That's a true statement, but utterly non-responsive to the point I was making.
Individual organisms are incredibly reliable when you consider the range of functions they perform. Compare, say, a quadcopter drone (or any other small air vehicle) with a parrot.
Lifespan without service or repair? Drone, weeks. Parrot, decades.
Autonomy before recharging/refueling? Drone, 20 minutes. Parrot, hours to days.
Cognitive faculties? Drone, slim to none. Parrot, long term autonomous in complex environments.
Reproduction? We can't build things that do that at all yet, let alone pack one into a 1kg autonomous aircraft.
Yes, we can build simple machines to replicate one function of a living creature, and those machines will be more reliable over short durations, but only because they are orders of magnitude simpler. You might as well call an LCD screen "unreliable" because it won't outlast a photograph.
From modern evolutionary biology's perspective "individual organisms" are NOT the "basic units/modules etc." of life. The basic ones are genes at the core informational level level and species at more loose and macro level.
So the living things to software analogy would be more like:
- gene == source code of a program's module (like an "independently testable unit of code" - natural-selection + sex-based recombination are actually the tests)
- ... (organizational levels with with no direct analogy to software go in between)
- individual organism == set of processes (running instances of programs) running together with heavy inter-process communication
Then at a higher level, genes and their manifestations constitute the "hardware" (more like a VM), run the software called "memes", with its own organizational patterns that are outside the field of biology.
What you call living thing or individual organism is, from "life's perspective", closer to a transient group of running processes that can be killed at any time because their sources and binaries are safely stored as genes or memes. Your body and your psychological self are closer to "running threads of nginx on a particular server handling a particular set of requests" than to "the program nginx itself" in source or binary form :)
Each living individual is an uninterrupted continuum of living cells (sometimes reduced to a single living gamete) back to the origin of life, whatever it was.
Compared to what? Some trees are very old. There's a bristlecone pine tree in California that has been around since before man knew how to smelt iron. What reproduces better than living things? Virtually nothing made by human beings is expected to last that long, let alone something as complex and intricate as a tree is. Some buildings, by luck and continuous maintenance, may last as long - but they don't self reproduce and only stay standing through massive ongoing repair.
True enough, but for every bristlecone pine or ancient yew tree, there are billions of bacteria that live mere days and insects that live a few weeks or months. In addition to vastly outnumbering them, I would wager that all the insects and bacteria of the world probably outweigh all the 500+ year old trees currently in existence.
To really stretch the analogy, there are also millions (perhaps billions) of short-lived, abandoned software projects that never grew into something big and reliable. They're less interesting because it's usually pretty obvious why they failed.
Oh? We don't even begin to have the technology to create a self-replicating, self-repairing machine that can be expected to last 70 years or so of active service. One that slowly gets better over time as the error-prone replication turns up the odd improvement.
You should not look at 'life' as single organisms but as a system of organisms and as such it is very reliable. Once it started it lasted for billions of years, and over time managed to exhibit an extreme shift in complexity using roughly the same basic mechanisms.
The only things we've made that are more reliable than life are buildings that don't move (and are still prone to catching fire every now and then), anything with moving parts needs constant maintenance to get even a couple of years of use out of it.
The answer to a slightly different question is quite simple: how did life get so reliable? First, we should define what it is that it is reliable at. Particular organisms are, of course, far from reliable, but if we look at life as a whole, it is very reliable in doing one thing: ensuring that at any time there's at least a single copy of the program (genetic matter) that is in a runnable condition. How is it so reliable at that?
1. The goal is rather simple.
2. The time and energy (the computational effort) required to arrive at that first viable self-replicating molecule was huge.
3. The computational effort of the constant required maintenance is also similarly huge.
It turns out software was only reliable in the dimensions we we carefully looking at.
I'm not sure 'proof' would have helped any - we might well have proved that, say, Flash could successfully display any valid animation you could throw at it without even thinking about whether it was also pwning your machine.
Proofs in software are more complicated than that. For something like flash, you could have proofs that it handles corrupt, either intentionally or unintentionally, data without blowing up.
Then again, I'm one to believe that we need to focus more on capabilities systems, and other ways to ensure applications can only do what they want to do. Look at something like the rowhammer attack. Being able to break out of a sandbox through completely valid code is something we should be looking at mitigating as well.
Not true in theory or in practice. "Undefined behaviour" has a specific meaning in terms of the C standard, distinct from "implementation-defined behaviour" like the size of int or size_t. And in practice, writing beyond the bounds of an array almost always leads to arbitrary code execution (remote in the case of a networked program), double free almost always leads to arbitrary code execution, signed integer overflow on newer compilers sometimes leads to arbitrary code execution, ...
Many, but I'm not sure most.
However they nearly all involve someone (be it the language designer, compiler writer or application writer) not thinking about all the malicious possibilities of the code in question. Because that's not the problem they're trying to solve right now, and they're only human. And I only use security vulnerabilities as an example - the next thing we're all not thinking about might be power consumption, or creating AI paradoxes, or whatever. But we're definitely not thinking about it, and no-ones going to be proving it.
> And I only use security vulnerabilities as an example - the next thing we're all not thinking about might be power consumption, or creating AI paradoxes, or whatever. But we're definitely not thinking about it, and no-ones going to be proving it.
I don't think you have to be thinking about it. Every time some new class of vulnerabilities has arisen, e.g. SQL injection, it just hasn't affected well-formed programs written with good tools, and certainly not verified programs. Correct programs just don't have these problems, as a side effect of being correct.
The problem with "proofs" is that software is often an iterative process because the environment and problems are constantly changing. If you have a fixed known problem you can do proofs to your hearts content, but in a changing environment you make the most of it with limited resources.
You don't have to proof everything. Eg just halting is good enough for a lot of things. (And this is not the general halting problem. Writing programs that provably halt is almost trivial.)
All programming is proof. You just don't often know what exactly it is you're proving.
Anyway, the point is moot: software is not that reliable. It's good at the common case, and is very brittle at the edge cases. That's my experience anyway.
Not so drab -- that sort of thinking can lead to a pretty big deal, namely,
the Curry-Howard Isomorphism[0]. From the linked WP page:
In other words, the Curry–Howard correspondence is the observation that two families of formalisms that had seemed unrelated—namely, the proof systems on one hand, and the models of computation on the other—were, in the two examples considered by Curry and Howard, in fact structurally the same kind of objects.
If one now abstracts on the peculiarities of this or that formalism, the immediate generalization is the following claim: a proof is a program, the formula it proves is a type for the program. More informally, this can be seen as an analogy that states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem ... and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run.
(Of course, in the context of those job interviews you mentioned, this sort of thing would probably be overkill, unless the job involved functional-programming...in which case, though, they might well not have asked you how your "skills in mathematics would transition to programming" in the first place :-) ).
I think it would be accurate to assert that mathematics helps create a logical thought processes which is the only way to think about programming. Additionally, some areas of mathematics are nearly identical to their programming counterparts (set theory, Boolean logic, graph theory, etc). When I am doing SQL joins it helps me to think about set theory/ven diagrams to envision the output. Additionally, I think the strictly defined terms in mathematics helps me articulate concepts relate to software both more accurately and precisely. For example, I can define an integer in most languages as the set of natural numbers union the set of additive inverses union the set containing only zero
The paper is talking about rigorous formal mathematical proofs of correctness like in the sense of of the seL4 kernel (https://sel4.systems/Info/FAQ/) where they have confirmed the kernel is completely free of bugs such as buffer overflows, null pointer exceptions, use-after-free, etc.
> Of course, there might be bugs in the specification (the proof the made was that the kernel matches the specification)
Nothing is perfect, but this approach catches more bugs than any other technique. Also, some specifications are simple to specify e.g. it's not hard to specify that an array index must be within the bounds of the array and if you did get this wrong you'd notice quickly as you'd be unable to prove obvious facts are correct.
Systems for processing highly classified governmental/military confidential information often are required (depending on the country laws) to provide formal proof of their entire work. Other than that (and because it is too expensive to run such an analysis) people just need to look at the code to check whether it's doing what it's supposed to do.
> Specialisation involves a deep commitment to a narrow selection of presentation, reasoning methods, paradigm, language and application area, or even a particular application. The whole point of the specialisation in formal methods is to restrict the notational framework as far as necessary to achieve some formal goal, but nevertheless to show that the restrictions do not prevent successful application to a surprisingly wide range of problems. This is the reason why specialist research into formal methods can run the risk of being very divisive. An individual researcher, or even a whole community of researchers, becomes wholly committed to a particular selection of specialisations along each of the axes: say an operational or an algebraic presentation of semantics, bisimulation or term rewriting as a proof method, … The attraction of such a choice can be well illustrated in certain applications, such as the analysis of the alternating bit protocol or the definition of the stack as an abstract data type. The perfectly proper challenge of the research is to push outwards as far as possible the frontiers of the convenient application of the particular chosen formalism. But that is also the danger: the rush to colonise as much of the available territory can lead to imperialist claims that deny to other specialisms their right to existence. Any suggestion of variation of standard dogma is treated as akin to treason. This tendency can be reinforced by the short-sightedness of funding agencies which encourage exaggerated claims to the universal superiority of a single notation and technique.
> The consequences of the fragmentation of research into rival schools is inevitable: the theorists become more and more isolated, both from each other and from the world of practice, where one thing is absolutely certain: that there is no single cure for all diseases. There is no single theory for all stages of the development of the software, or for all components even of a single application program. Ideas, concepts, methods, and calculations will have to be drawn from a wide range of theories, and they are going to have to work together consistently, with no risk of misunderstanding, inconsistency or error creeping in at the interfaces. One effective way to break formal barriers is for the best theorists to migrate regularly between the research schools, in the hope that results obtained in one research specialisation can be made useful in a manner acceptable by the other. The interworking of theories and paradigms can also be explored from the practical end by means of the case study, chosen as a simplified version of some typical application. In my view, a case study that constructs a link between two or more theories, used for different purposes at different levels of abstraction, will be more valuable than one which merely presents a single formalisation, in the hope that its merits, compared with rival formalisations, will be obvious. They usually are, but unfortunately only to the author.
> There is no single theory for all stages of the development of the software, or for all components even of a single application program. Ideas, concepts, methods, and calculations will have to be drawn from a wide range of theories, and they are going to have to work together consistently, with no risk of misunderstanding, inconsistency or error creeping in at the interfaces.
I'm not convinced. I remain hopeful that one or other technique will show itself adequate for complete coverage of real-world programs. Compare programming languages - naïvely one would think different languages have different specializations and it's important for programmers to be fluent in a wide variety of them and good at interfacing between different languages. But I'm increasingly coming to believe that good general-purpose languages are possible and that better systems are built in a single language, by programmers specialized to that language.
Ah, but there's a difference between formal verification and programming languages. The problem of general formal verification (known in general as the model-checking problem[1], regardless of the approach used which could be model-theoretic or proof-theoretic) is literally the hardest problem in all of computer science. Any computational problem can be reduced in polynomial time to program verification (i.e. model checking). In fact, all NP-complete and PSPACE-complete problems are trivially reduced. Finding a general tractable solution (even if it includes human intelligence) is therefore a mathematical impossibility. The best we hope for is a solution that is applicable to programs people write. The question is then whether there is one well defined "class" of programs humans write to which an efficient algorithm (again -- even one involving humans in the loop) applies. So far results from decades of verification research show that this is not the case, and there are at least several such classes, but maybe the classes aren't general enough. If humans are part of the algorithm (e.g. interactive proofs, manual dependent types), the class might be wide, but our experience has shown that verifying programs in this way takes tremendous effort, even for small programs, and even when the programs are kept especially simple for the sake of verification. Even if there is a solution that is applicable to most (I'll settle for most) programs, it is so far nowhere in sight. Most efforts are directed at finding partial solutions for specific domains.
[1]: Called that because it is the problem of checking whether a given program is a satisfying theory -- i.e. a model -- for the given logical property.
That it's a hard problem doesn't necessarily mean we're approaching it wrong. Indeed the fact that it's mathematically proven to be hard offers some confidence that we might not be.
Are there examples of cases where a system was very hard to verify with any one general technique, but much more practical to verify by using several domain-specific techniques and some kind of bridge between them (i.e. not simply coming up with a general approach for which the specialized techniques were, well, specializations - since as far as I can tell your quote is advocating for something different)?
> Are there examples of cases where a system was very hard to verify with any one general technique, but much more practical to verify by using several domain-specific techniques and some kind of bridge between them
I'm not sure what you mean by bridge but the halting problem comes to mind: the general case is impossible but you can prove common algorithms halt by showing they're structurally recursive (the recursive parameter always get smaller) or some metric always decreases on the recursive call (e.g. the sum of the length of two lists always gets smaller on the recursive call).
> you can prove common algorithms halt by showing they're structurally recursive (the recursive parameter always get smaller) or some metric always decreases on the recursive call (e.g. the sum of the length of two lists always gets smaller on the recursive call)
Right, but those are just special cases of the same technique - you can combined them by using dependent types to lift the list length to the type level and then this metric technique is just a special case of structural recursion.
Dependent types are not a verification technique. They are just one way of encoding statements about your program (in intuitionistic logic). The technique to prove those statement are either manual or manually-assisted (e.g. Coq), or automated using various model-checking algorithms (Liquid types). Deciding to encode program properties in dependent types (e.g. Idris) or direct logic (e.g. Java+JML) doesn't make verification any easier or harder. It's just a form of stating the properties you wish to verify.
Sure. What I'm saying is that you can encode statements about values and statements about types the same way, by using dependent types, and once you do that then you can verify halting of metric-recursive functions using exactly the same approach that you use to verify halting of structurally-recursive functions. So proving halting using a combination of proofs that metric-recursive functions halt and proofs that structurally-recursive functions halt isn't an example of it being useful to use two different approaches for different parts of the proof of correctness of a program, and doesn't make the case for having multiple approaches to verification and bridges between them.
That depends on what you mean by "exactly the same approach". Can the same algorithm construct both proofs? Can it construct both proofs with the same computational complexity? If not, then you're not using the same approach.
Using dependent types is more of a particular notation than a solution to verification. How you prove your type inference/checking is the hard part. Examples of approaches include SAT/SMT solvers, symbolic model checking, manual deduction, explicit model checking, abstract interpretation (which is really abstraction + explicit model checking; H-M inference algorithms can be described in terms of this approach), weakest preconditions, etc. You can use all of these approaches to infer/check dependent types, just as you can use them to verify program logic stated using means other than dependent types.
> That depends on what you mean by "exactly the same approach". Can the same algorithm construct both proofs? Can it construct both proofs with the same computational complexity?
Yes, because once you're representing the values with dependent types, metric recursion and structural recursion are physically the same thing.
> Dependent types are not a verification technique...Deciding to encode program properties in dependent types (e.g. Idris) or direct logic (e.g. Java+JML) doesn't make verification any easier or harder.
For what it's worth, every time I see articles and comments about the use of formal verification in general purpose programming around here, I never see any mention of how the actual verification part requires incredibly challenging manual proofs. In particular, I see articles about dependent types that give the impression you get the proofs for free when that isn't the case.
Let me respond to that with a quote from "No Silver Bullet, Refired", by another Turing Award winner, Fred Brooks:
> Even if "NSB" were universally seen as pessimistic, what is wrong with that? Is Einstein's statement that nothing can travel faster than the speed of light "bleak" or "gloomy?" How about Godel's result that some things cannot be computed? "NSB" undertakes to establish that "the very nature of software makes it unlikely that there will ever be any silver bullets." Turski, in his excellent response paper at the IFIP Conference, said eloquently:
>> Of all misguided scientific endeavours, none are more pathetic than the search for the philosophers' stone, a substance supposed to change base metals into gold. The supreme object of alchemy, ardently pursued by generations of researchers generously funded by secular and spiritual rulers, is an undiluted extract of wishful thinking, of the common assumption that things are as we would like them to be. It is a very human belief. It takes a lot of effort to accept the existence of insoluble problems. The wish to see a way out, against all odds, even when it is proven that it does not exist, is very, very strong. And most of us have a lot of sympathy for these courageous souls who try to achieve the impossible. And so it continues. Dissertations on squaring a circle are being written. Lotions to restore lost hair are concocted and sell well. Methods to improve software productivity are hatched and sell very well. All too often we are inclined to follow our own optimism (or exploit the optimistic hopes of our sponsors). All too often we are willing to disregard the voice of reason and heed the siren calls of panacea pushers.
> Turski and I both insist that pipe-dreaming inhibits forward progress and wastes effort.
> So we come back to fundamentals. Complexity is the business we are in, and complexity is what limits us. R. L. Glass, writing in 1988, accurately summarizes my 1995 views:
>> So what, in retrospect, have Parnas and Brooks said to us? That software development is a conceptually tough business. That magic solutions are not just around the corner. That it is timefor the practitioner to examine evolutionary improvements rather than to wait—or hope—for revolutionary ones.
>> Some in the software field find this to be a discouraging picture. They are the ones who still thought breakthroughs were near at hand.
>> But some of us—those of us crusty enough to think that we are realists—see this as a breath of fresh air. At last, we can focus on something a little more viable than pie in the sky. Now, perhaps, we can get on with the incremental improvements to software productivity that are possible, rather than waiting for the breakthroughs that are not likely to ever come.
---
So discussing some methods of formal verification (such as manually checking dependent types) as a solution is like saying a particle accelerator is the solution to the alchemist's problem. Theoretically it can work; in practice, it's often too much effort :)
Personally I'm not sure pipe-dreams inhibit forward progress, but they sure do generate a lot of noise...
I'm not convinced it is necessarily that challenging, because the proof goes with the code. A program source is already an informal proof of correctness - the reason we tend to believe our programs are correct is that their code looks like it does the correct thing. Few maintainable programs rely on invariants that appear "magically" out of nowhere; a human reader would believe an invariant held because they could see a code path or state that represented that invariant. I think for most real-world code, the theorem that the code represents (in a Curry-Howard sense) tends to be trivial.
> I'm not convinced it is necessarily that challenging, because the proof goes with the code. A program source is already an informal proof of correctness - the reason we tend to believe our programs are correct is that their code looks like it does the correct thing. Few maintainable programs rely on invariants that appear "magically" out of nowhere; a human reader would believe an invariant held because they could see a code path or state that represented that invariant.
Have you done any formal proofs before? You're severely underestimating how difficult and time consuming they are to do even if you do have some intuition about why they are correct. The sel4 microkernel took around 5 years for around 20 experts to verify for example. Verifying a program can result in you having to prove arbitrarily difficult maths theorems so it's similar to saying automating arbitrarily difficult maths theorems should be trivial.
> I think for most real-world code, the theorem that the code represents (in a Curry-Howard sense) tends to be trivial.
Yes, the theorem/specification statement may be trivial compared to the code but the hard part is coming up with the proof that shows the code matches the specification. You don't get this for free.
> Verifying a program can result in you having to prove arbitrarily difficult maths theorems so it's similar to saying automating arbitrarily difficult maths theorems should be trivial.
But you wouldn't write a program that depended on a theorem that wasn't proven, no? I mean often the only mathematically hard parts of a given program are in the libraries it uses - which could ship with their own proofs.
> Yes, the theorem/specification statement may be trivial compared to the code but the hard part is coming up with the proof that shows the code matches the specification. You don't get this for free.
Doesn't the structure of the code tell you how to structure the proof though? Like, if you've written code that appends to a list by appending a single element and recursing, the way you prove it correct is to prove that it appends a single element and that it recurses correctly. If you've written something that's supposed to be a sorting algorithm and the code rearranges the elements of a list, why is it that you believe this particular rearrangement of the elements is a correct sort? Isn't the answer to that question your proof of correctness?
> Isn't the answer to that question your proof of correctness?
If that were the case then we'd never have bugs :) The number of corner cases can be staggering. So the answer to "why do you believe a sorting algorithm sorts?" is "because I considered a few cases, in the hope that it's enough". Whether or not it actually is enough is the source of all bugs.
Just take a look at the state-space visualizations of real but positively tiny programs to understand how complex tiny, useful programs are: https://www3.hhu.de/stups/prob/index.php/State_space_visuali... Some seem structured enough (those are the toy examples), but some are far from it.
Or at this program that is known to never throw an exception, yet proving it is... hard:
int foo(int x) {
if (x <= 2 || (x & 1) != 0) return 0;
for (int i = 2; i < x; i++)
if (bar(i) && bar(x - i)) return i;
throw new AssertionError(); // unreachable
}
boolean bar(int x) {
for (int i = 2; i < x; i++)
for (int s = x; s >= 0; s -= i)
if (s == 0) return false;
return true;
}
Does this seem like an arbitrarily difficult math theorem (because it is)? See those two lines in the middle of `bar` where the result depends on the depth of the recursion (or loop)? That's what makes the proof incredibly hard, and it is very common in real world programs. Does the structure of the code suggest a proof?
Writing this program in Idris and proving that the type of `foo` is `Int` rather than `Maybe Int` is equivalent to proving Goldbach's conjecture.
True, most functions don't look like this, but in pretty much every serious project I've seen, there were at least a couple of instances of code that is even more complicated.
Now, the real question is where do the expensive bugs lie. In code that's hard to prove or in code that's easy to prove (or equally in both)? That is a question that is certainly worth investigating. But wherever the expensive bugs lie, it's likely not in implementations of list append...
> See those two lines in the middle of `bar` where the result depends on the depth of the recursion (or loop)? That's what makes the proof incredibly hard, and it is very common in real world programs
Not my experience, but shrug.
> Does the structure of the code suggest a proof?
No - but it does look like bad code.
> True, most functions don't look like this, but in pretty much every serious project I've seen, there were at least a couple of instances of code that is even more complicated.
I've seen code that looks like that, but it's always been easy enough to clear up. As my career goes on I'm starting to think that almost all real-world code is trivial.
> Now, the real question is where do the expensive bugs lie. In code that's hard to prove or in code that's easy to prove (or equally in both)?
My experience is that most production bugs are stupidly obvious things. And that possibly all bugs are either stupid "why doesn't the compiler catch that" cases, or code that is bad (unreadable) on its face. Possibly that's a tautology.
> But wherever the expensive bugs lie, it's likely not in implementations of list append...
You say that, but verification of JDK sorting uncovered a real bug.
> I'm starting to think that almost all real-world code is trivial.
We're working in very different worlds, then. Sure, maybe in CRUD webapps almost all code is trivial, but if it's trivial then bugs aren't that tricky anyway. But the code that runs distributed database clusters, or avionics software, is far from trivial, and we know (from years of software verification) that verifying that code is essentially hard.
> My experience is that most production bugs are stupidly obvious things. And that possibly all bugs are either stupid "why doesn't the compiler catch that" cases, or code that is bad (unreadable) on its face.
In that case you would see much bigger productivity differences between languages like Haskell and languages like Python, while most (admittedly scarce) data shows that the differences are tiny.
> but verification of JDK sorting uncovered a real bug.
That is a very complicated sorting algorithm, and uncovering it wasn't done automatically, but required hard work. It is precisely an example of small code that is complex, and while formal verification is possible (because it's small), it is not trivial and not automatic. In any event, that code had more to do with my Goldbach example and much less to do with list append. Proving it was nowhere near as trivial as proving append.
> In that case you would see much bigger productivity differences between languages like Haskell and languages like Python, while most (admittedly scarce) data shows that the differences are tiny.
My cynical hypothesis would be that Haskell really does lower the defect rate by an order of magnitude or more in comparison to Python (in terms of e.g. correct handling of edge cases), but this doesn't noticeably impact productivity/business value for many use cases.
> But you wouldn't write a program that depended on a theorem that wasn't proven, no? I mean often the only mathematically hard parts of a given program are in the libraries it uses - which could ship with their own proofs.
Proofs for nontrivial programs quickly get into undecidable areas in terms of proof automation. You might have relevant theorems lying around but how you combine them to create your proof is an undecidable problem.
As an example, if you have integer theorem statement where you can only multiply variables by constants (e.g. x * 5 + y * 2 ... = x * 2 + ...) there's an algorithm that can always find a proof. If you relax this restriction, no such algorithm does or can exist that will always find a proof.
> Doesn't the structure of the code tell you how to structure the proof though? Like, if you've written code that appends to a list by appending a single element and recursing, the way you prove it correct is to prove that it appends a single element and that it recurses correctly.
Usually you'd use inductive proofs to write those kinds of proofs and the induction scheme you use would follow the way recursion is done in the program. That doesn't mean the gaps in the proofs (e.g. base and step case) are trivial though.
> If you've written something that's supposed to be a sorting algorithm and the code rearranges the elements of a list, why is it that you believe this particular rearrangement of the elements is a correct sort? Isn't the answer to that question your proof of correctness?
The jump from a rough intuition about why something is provable to a proof is much larger than you'd think. I'd recommend following a tutorial on Coq. It's worthwhile even if you don't go beyond a quick look so you can appreciate the almost vertical learning curve if you're not well versed in maths and logic (which most programmers aren't) and how proving simple facts rigorously (e.g. "list_reverse (list_reverse x) = x") requires a lot of effort.
Sure. In fact, I believe this is the norm rather than the exception. Software systems often use model-checkers, abstract interpretation and manual deduction to be verified. Each have their strengths and weaknesses. In fact, you can see all three methods used in one of the common representations of logic (which I've picked because I know you're a Scala guy): types. Simple types (like H-M types) perform crude abstract interpretation, but can only prove properties of finite state machines. Liquid types use model-checking algorithms to infer and check some kinds of dependent types. These, however, still don't cover all properties, so in practice, people need to resort to manually-inferred/checked dependent types. Using those alone would be extremely cost prohibitive.
In the safety-critical software world, you see projects using model checkers to verify individual modules and deductive proofs (say, in Isabelle) to verify the interaction among modules or vice-versa. In the less-safety-critical software world, you see people commonly use static analyzers (employing abstract interpretation), even though those can only verify certain properties, because both interactive deductive proof and automatic model checking are too cost prohibitive.
But the problem in general is this: we are not at a point where any single approach nor a combination of several lets us fully verify a real-world program even of moderate side at any acceptable cost. I don't believe any moderately-sized program has ever been fully verified using any technique.
> But the problem in general is this: we are not at a point where any single approach nor a combination of several lets us fully verify a real-world program even of moderate side at any acceptable cost. I don't believe any moderately-sized program has ever been fully verified using any technique.
Sure. Which means I think we simply don't know enough to say one way or the other what kind of approach we will need for effective proofs. Maybe we will need to combine multiple techniques and have bridges between them. But maybe we really will be able to extend one particular technique to cover all the important cases, or find a single general approach that recovers all the useful techniques we've found so far as special cases.
Right. But it is important to understand that this is the hardest problem in computer science (human-level AI is much easier), and so general-enough solutions must somehow be aligned with how humans tend to construct programs (because a completely general solution is impossible, and solutions that are not aligned with how people program can only hope to solve human-produced code by accident). For example, we do know that we cannot create a general-purpose language that will make verification easy for all programs written in it; that is a mathematical impossibility. Whatever approach may work one day, it will have to be based on empirical observations of programs people tend to write.
> For example, we do know that we cannot create a general-purpose language that will make verification easy for all programs written in it; that is a mathematical impossibility.
Not true. We know that we cannot create a Turing-complete language with that property. We haven't proven that we'll never be able to create a general-purpose non-Turing-complete language. I might argue that Idris is already an example of such a thing.
> We haven't proven that we'll never be able to create a general-purpose non-Turing-complete language.
Well, if you're referring to total languages, then they are Turing complete for all intents and purposes.
Total languages are not immune to the halting problem (or, rather, to its finite generalizations known as "bounded halting"). The classical formulation of the halting problem simply tells you that verifying a program in general is undecidable. But this is simply because a Turing machine is a finite structure that can describe an infinite one. So in some way, the halting problem is undecidable in the same way that finding the maximum or sorting an infinite list doesn't terminate. Yet once the list is finite (or the Turing machine is known to terminate), you then need to ask yourself how hard is it to find the maximum element in a finite list, how hard is it to sort it, and how hard is it to verify a program that is known to terminate? The answers to all these questions are well known, and quite different from one another. Finding the maximum takes Ω(n) (worst-case), sorting is Ω(n lg n), and verification is Ω(|S|), namely at least linear in the number of states the program takes until it terminates (this directly follows from a trivial generalization of the halting problem called "bounded halting"). So sure, total programs are known to terminate, and all we have left to do now to prove them correct is to overcome a super-exponential lower complexity bound... In practice that is just as undecidable as for programs that are not proven to terminate.
And, BTW, the lower complexity bounds for verification of finite state machines written in expressive languages is already PSPACE-complete. There cannot be a useful general programming language with verification bounds that are less than exponential (unless, that is, PSPACE=P); but that is a good thing: verification of total-functional programs is super-exponential. So my point is that even completely general verification of freakin' finite state machines is out of our reach in large-enough programs. It's doubtful you can find a useful computational model that's simpler.
Also, notice that any program could trivially be made total without changing its semantics. Give me a program you want verified, I'll add a decreasing counter starting with 10100 to all its loops/recursions, and now your program is total and you'll never know the difference. Does that make it any easier to verify?
The total-language people know this. They don't claim that this makes practical program verification any easier. In fact, the motivation for totality has nothing to do with program verification but with using C-H to prove general mathematical theorems. Non-termination, as you know, is the same as inconsistencies in those proofs (although not in proofs about programs; non-termination introduces no inconsistency to those). However, some people who are only familiar with the classical formulation of the halting theorem have concluded that totality => no halting problem => verification is possible! This is false, and was abundantly clear even in the 50s. Kurt Gödel, in a letter to von Neumann in 1956, mentions in passing this finite (and obvious) generalization of the halting theorem before raising (for the first time!) the question of P vs. NP.
> even completely general verification of freakin' finite state machines is out of our reach in large-enough programs. It's doubtful you can find a useful computational model that's simpler.
Eh, maybe. I find it very hard to reason about finite state machines in programs as a human, so it doesn't surprise me that proving correctness properties about them would be hard. I'm not at all convinced that a general-purpose programming language necessarily includes support for fully general finite state machines.
> Also, notice that any program could trivially be made total without changing its semantics. Give me a program you want verified, I'll add a decreasing counter starting with 10100 to all its loops/recursions, and now your program is total and you'll never know the difference. Does that make it any easier to verify?
Yes - it eliminates the class of errors where one has "implemented" something by an infinite loop. It helps for concrete programs in the same way that it helps for theorems, no?
Technically yes, but as Scott Aaronson says, a universe where P=NP would probably look very different from ours (and PSPACE is harder than NP). In any event, verifying effectively Turing-complete languages (even total ones) is much harder than EXPTIME (and we know that EXPTIME > P).
> I find it very hard to reason about finite state machines in programs as a human
I didn't mean it like that (programming with explicit states). Just a model of computation where the number of states is bounded. Any program with finite memory is a finite state machine. Every language must support at least that.
> it eliminates the class of errors where one has "implemented" something by an infinite loop. It helps for concrete programs in the same way that it helps for theorems, no?
No, because when you prove a program property A you know that you've really proven "A or no-termination". So being able to prove any property is not an inconsistency. This is not the case for mathematical theorems that don't have running time, and where "no termination" is meaningless. If running time is 0, then A just means A, and if A is a contradiction then you have a real problem.
Now, what about eliminating non-termination from programs? Well, you're not really doing that either, because as far as we're concerned, a program that takes 10^100 steps doesn't really terminate at all. One could claim that people are more likely to accidentally write a function that loops forever than one that loops 2^64 times. This may be true, but this again relies on empirical facts rather than general mathematical properties.
In any case, what makes you think that languages like Idris may make verification easy? The few cases of programs verified in this mostly-manual way took years to prove, even for very small and intentionally "dumbed down" code.
> I didn't mean it like that (programming with explicit states). Just a model of computation where the number of states is bounded. Any program with finite memory is a finite state machine. Every language must support at least that.
Any program is (or can be modeled as) a finite state machine, sure. But useful programs are a small subset of the space of possible finite state machines. It's not beyond hope that we could find a subset that allowed us to write most useful programs but was easier to reason about.
> One could claim that people are more likely to accidentally write a function that loops forever than one that loops 2^64 times. This may be true, but this again relies on empirical facts rather than general mathematical properties.
I am worried about not-terminating-in-reasonable-time (though much less worried than I am about looping forever), but can't we just make that one of the properties we keep track of and prove with the same tools?
> In any case, what makes you think that languages like Idris may make verification easy? The few cases of programs verified in this mostly-manual way took years to prove, even for very small and intentionally "dumbed down" code.
I guess my experience that keeping track of more properties in the type system doesn't make coding any harder. Compare Rust - writing Rust programs essentially means proving that things have valid lifecycles and are not used outside of them. This is a complex property that mainstream programmers were not previously proving at all - that many had despaired of ever being able to prove. And yet in practice people who write Rust find that not only can they do it, but the additional proof effort quickly becomes barely noticeable. Likewise with Idris you're proving termination in finite (though possibly unreasonable) time and once you get used to doing that it doesn't actually seem noticeably harder than not doing so. So I'm kind of hopeful that we can just keep improving the type systems used by mainstream programming languages until writing a program naturally includes proving the important properties of that program without even noticing.
> It's not beyond hope that we could find a subset that allowed us to write most useful programs but was easier to reason about.
It is beyond hope that we find a subset that's generally easier to reason about. Verifying one line programs of this sort:
if (a && ~b || c || ~d && e ...)
crash()
is already NP-complete (SAT). Adding some loops that are of depth 2 makes it PSPACE-complete (TQBF, aka QSAT). I can't think of a useful programming language that doesn't have even small-constant-depth loops (which makes it finite state) and simple boolean algebra. Software verification is about verifying some subsets of programs that humans happen to write. It is categorically impossible to write a general-purpose language where all programs are easier to verify than PSPACE.
> but can't we just make that one of the properties we keep track of and prove with the same tools?
Sure, with super-exponential complexity :) But again, this is in the worst case. We hope that humans usually write programs that are simpler.
> I guess my experience that keeping track of more properties in the type system doesn't make coding any harder.
If you mean H-M types as in Haskell, then the properties those types enforce are either trivial (i.e. true for all programs, e.g. function returns Int), or a result of a finite state machine (that's the proving strength of H-M types). You cannot prove even a single bit of a program's output that's a result of non-constant-depth recursion (there's a special case for recursion which is of depth that's a constant multiple of the input length, like `map`). If we take Haskell, you can replace each of your functions with constant-depth recursion (0 or 1 would suffice in virtually all circumstances) and the program will still typecheck yet will be completely wrong.
As for Rust's linear types, that is precisely what I'm talking about. A certain class of bugs (memory errors) that humans are known to make and that verifying with abstract interpretation is easy. That's what software verification aims to do. We cannot hope of proving general programs generally correct, regardless of the language they're written in.
BTW, thinking of type systems muddles understanding in this case, because type systems are just notation. The verification taking place in most sound type systems is abstract interpretation. Yes, we can find more important properties to verify with abstract interpretation, but it has been proven that some properties will forever elude abstraction.
The way abstract interpretation works is that it translates the program into an "abstract" program which is just a finite state machine, with the number of states equal to the number of concrete types, and running an exhaustive model checker on that; this means that the complexity of inferring this kind of types is Ω(|S|), namely, linear in the number of concrete types. As abstract types can multiply the number of concrete types, the inference can become exponential in the worst-case, but it usually doesn't. Once you introduce dependent types, the algorithm is still Ω(|S|) -- linear in the number of state, i.e. types -- but now the number of types is unbounded, and so the problem becomes undecidable.
> until writing a program naturally includes proving the important properties of that program without even noticing.
You're right, but this entirely depends on which properties are found to be important (and has little to do with type systems specifically; again, this is mostly notation[1]), and that, in turn, is rather empirical.
> I can't think of a useful programming language that doesn't have even small-constant-depth loops (which makes it finite state) and simple boolean algebra. Software verification is about verifying some subsets of programs that humans happen to write. It is categorically impossible to write a general-purpose language where all programs are easier to verify than PSPACE.
Eh. Again, I don't think we necessarily need arbitrary boolean algebra - something that's hard enough to reason about as a human - and may be able to capture the valuable use cases in a simpler model. Fundamentally if we have any hope of doing verification at all, surely we can characterize the constraints we need for verification and then push them back to the programming language level.
> If we take Haskell, you can replace each of your functions with constant-depth recursion (0 or 1 would suffice in virtually all circumstances) and the program will still typecheck yet will be completely wrong.
Could you expand on this / give an example? I don't think I follow. And I take it from what you're saying that this doesn't apply if we permit dependent types?
> BTW, thinking of type systems muddles understanding in this case, because type systems are just notation. The verification taking place in most sound type systems is abstract interpretation. Yes, we can find more important properties to verify with abstract interpretation, but it has been proven that some properties will forever elude abstraction.
Properties that are important for real-world programs? Abstract interpretation sounds very similar to how we reason about programs as humans. It just seems like to the extent that we understand how to do something at all we should be able to formalize that understanding.
If we're talking about using programs to address open questions - a best-effort at the travelling salesman problem, say - then I can see how you might end up with a program that had a pile of heuristics that seemed to work but with no concrete understanding of how or if it worked - except that even then you'd probably use a well-known, formally validated heuristic rather than using the program as a medium for mathematical research. I just think (empirically) it would be very rare as a business requirement to need to do something completely unproven, and therefore it might be possible to have a useful general-purpose programming language that didn't allow doing that.
> Fundamentally if we have any hope of doing verification at all, surely we can characterize the constraints we need for verification and then push them back to the programming language level.
That is not what the verification community is trying to do at all, because trying to find a language that is not even NP-complete to verify and is still generally is absolutely impossible (explanation later). What the verification community is trying to do is to come up with approaches that make it possible/easy to verify some code, which is hopefully the majority of code. As far as languages go, the hope is that a language can make some verification of some code easier than in other languages. A general-purpose language that is at least useful in some cases, and in which all programs are easily verifiable can only exist if P=NP. The reason is this: at best, you can hope that the proof of correctness is checkable in polynomial time. This puts it in NP. If constructing a proof of correctness is possible in polynomial time, so is coming up with the solution in the first place. Namely, such a language wouldn't even need to be programmed. It will be a constraint solver (that somehow is in P). SQL minus boolean expressions might be the best you could do. Possibly useful, but certainly not general-purpose.
> Properties that are important for real-world programs?
Yes, and they are quite common in distributed algorithms.
> It just seems like to the extent that we understand how to do something at all we should be able to formalize that understanding.
Yet we can't because when we reason about something we assume a certain regularity of the state-space, that is often wrong in practice. That link I showed you where there are visualizations of state spaces, shows the one for the CAN bus protocol. It is the most complicated example on that page, and it is the very real protocol used by different components in your car that need to communicate.
> I just think (empirically) it would be very rare as a business requirement to need to do something completely unproven
That depends a lot on what you do. If you design schedulers for OS kernels, concurrent data structures, or distributed algorithms you see that these difficult cases are the rule rather than the exception.
I work on concurrent and distributed algorithms, and I do formal verification (TLA+ is my current tool of choice) most day every day. TLA+ offers both a theorem prover (a la Isabelle/Coq/Agda) as well as a model checker. Manual deductive proofs are virtually never worth the trouble (that would take me years), and even with a model checker -- where you just press a button and if there's a bug, any bug, you get a full trace of the execution that led to the bug -- it's still a lot of work, because distributed algorithms are just essentially complex.
> But maybe we really will be able to extend one particular technique to cover all the important cases, or find a single general approach that recovers all the useful techniques we've found so far as special cases.
This is like saying we need to extend individual AI algorithms that can play chess, Go, poker, drive a car etc. to a single algorithm that can do all of these things.
> This is like saying we need to extend individual AI algorithms that can play chess, Go, poker, drive a car etc. to a single algorithm that can do all of these things.
I think there are different models for conceptualising and expressing programs that are more appropriate for different situations, and in that sense we will always have specialisation.
However, I think in the future we will increasingly consider programming models separately from the language used to express them, and in that sense there will be completely general programming languages. Powerful bases to create the models themselves as libraries and DSLs.
Surely code you haven't proved correct is going to have way more bugs in it than code you tried to prove is correct? Maybe I'm misunderstanding but this quote is always posted as if it's some kind of rebuttal against formal methods.
I think the point he was making is that while its been proven to correctly do what it was built to do, that may not actually be anything like what the user needs it to do.
How many intricately specified software projects have failed because the spec bore no correlation to user needs?
I always thought that correctness (in computer science) only asserted that an algorithm acted as specified. For example, say the specification was: The input accepts an element in the set of real numbers, and the corresponding output is that number added to the next element in the set of natural numbers.
If this algorithm is used to dispense some type of medication, and I enter 3.1 and it murders you with 10 grams of alprazolam... well.... the algorithm is still correct.
> I always thought that correctness (in computer science) only asserted that an algorithm acted as specified. For example, say the specification was: The input accepts an element in the set of real numbers, and the corresponding output is that number added to the next element in the set of natural numbers.
Nobody is saying the formal proof approach will find all bugs, just that it helps find more bugs compared to not using it. You could make the same argument with acceptance testing: unless you specifically tried 3.1 as the input during testing, it might not give you the output you expect. Formal proof can be complimentary to traditional automated tests and QA.
I've always parsed this quote as "Beware of bugs in the above code; I have only proved that the code is correct, I haven't actually compiled and tested it."
For any non-trivial code, no matter how much formal analysis you do, you don't trust it until it's been properly tested.
I haven't gotten a chance to read the entire paper however the reference to the Therac-25 in the beginning was slightly tilted. Yes - it was a programmatic error that dispersed a deadly amount of radiation. But, if I remember correctly, the Therac-25 is often used in Software/Computer Engineering ethics classes as an instance in which a hardware safety mechanism would be appropriate. So while the article is right that a software malfunction did disperse a deadly amount of radiation, the fix for this isn't necessarily a software solution
83 comments
[ 4.8 ms ] story [ 139 ms ] threadHaving a single instance of a particular organism last for a long time just isn't what life is about. If you look at the full context of what life is doing, it is way goddamn more reliable than anything humans have designed, proofs or not.
Lifespan without service or repair? Drone, weeks. Parrot, decades.
Autonomy before recharging/refueling? Drone, 20 minutes. Parrot, hours to days.
Cognitive faculties? Drone, slim to none. Parrot, long term autonomous in complex environments.
Reproduction? We can't build things that do that at all yet, let alone pack one into a 1kg autonomous aircraft.
Yes, we can build simple machines to replicate one function of a living creature, and those machines will be more reliable over short durations, but only because they are orders of magnitude simpler. You might as well call an LCD screen "unreliable" because it won't outlast a photograph.
So the living things to software analogy would be more like:
- gene == source code of a program's module (like an "independently testable unit of code" - natural-selection + sex-based recombination are actually the tests)
- ... (organizational levels with with no direct analogy to software go in between)
- individual organism == set of processes (running instances of programs) running together with heavy inter-process communication
Then at a higher level, genes and their manifestations constitute the "hardware" (more like a VM), run the software called "memes", with its own organizational patterns that are outside the field of biology.
What you call living thing or individual organism is, from "life's perspective", closer to a transient group of running processes that can be killed at any time because their sources and binaries are safely stored as genes or memes. Your body and your psychological self are closer to "running threads of nginx on a particular server handling a particular set of requests" than to "the program nginx itself" in source or binary form :)
Each living individual is an uninterrupted continuum of living cells (sometimes reduced to a single living gamete) back to the origin of life, whatever it was.
The only things we've made that are more reliable than life are buildings that don't move (and are still prone to catching fire every now and then), anything with moving parts needs constant maintenance to get even a couple of years of use out of it.
1. The goal is rather simple. 2. The time and energy (the computational effort) required to arrive at that first viable self-replicating molecule was huge. 3. The computational effort of the constant required maintenance is also similarly huge.
Then again, I'm one to believe that we need to focus more on capabilities systems, and other ways to ensure applications can only do what they want to do. Look at something like the rowhammer attack. Being able to break out of a sandbox through completely valid code is something we should be looking at mitigating as well.
(We could also have used memory-safe languages)
I mean, pretty much the same way as int or size_t has a machine type size dependency
I don't think you have to be thinking about it. Every time some new class of vulnerabilities has arisen, e.g. SQL injection, it just hasn't affected well-formed programs written with good tools, and certainly not verified programs. Correct programs just don't have these problems, as a side effect of being correct.
Anyway, the point is moot: software is not that reliable. It's good at the common case, and is very brittle at the edge cases. That's my experience anyway.
The language (spec) is my set of axioms, the standard library existing theorems, and my program the proof.
It's kinda drab now that I think about it, but for a 'firing from the hip' answer I still stand by it.
In other words, the Curry–Howard correspondence is the observation that two families of formalisms that had seemed unrelated—namely, the proof systems on one hand, and the models of computation on the other—were, in the two examples considered by Curry and Howard, in fact structurally the same kind of objects.
If one now abstracts on the peculiarities of this or that formalism, the immediate generalization is the following claim: a proof is a program, the formula it proves is a type for the program. More informally, this can be seen as an analogy that states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem ... and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run.
(Of course, in the context of those job interviews you mentioned, this sort of thing would probably be overkill, unless the job involved functional-programming...in which case, though, they might well not have asked you how your "skills in mathematics would transition to programming" in the first place :-) ).
[0] https://en.wikipedia.org/wiki/Curry–Howard_correspondence
Nothing is perfect, but this approach catches more bugs than any other technique. Also, some specifications are simple to specify e.g. it's not hard to specify that an array index must be within the bounds of the array and if you did get this wrong you'd notice quickly as you'd be unable to prove obvious facts are correct.
Have you seen the specification for sel4? It's fairly complex.
> The consequences of the fragmentation of research into rival schools is inevitable: the theorists become more and more isolated, both from each other and from the world of practice, where one thing is absolutely certain: that there is no single cure for all diseases. There is no single theory for all stages of the development of the software, or for all components even of a single application program. Ideas, concepts, methods, and calculations will have to be drawn from a wide range of theories, and they are going to have to work together consistently, with no risk of misunderstanding, inconsistency or error creeping in at the interfaces. One effective way to break formal barriers is for the best theorists to migrate regularly between the research schools, in the hope that results obtained in one research specialisation can be made useful in a manner acceptable by the other. The interworking of theories and paradigms can also be explored from the practical end by means of the case study, chosen as a simplified version of some typical application. In my view, a case study that constructs a link between two or more theories, used for different purposes at different levels of abstraction, will be more valuable than one which merely presents a single formalisation, in the hope that its merits, compared with rival formalisations, will be obvious. They usually are, but unfortunately only to the author.
I'm not convinced. I remain hopeful that one or other technique will show itself adequate for complete coverage of real-world programs. Compare programming languages - naïvely one would think different languages have different specializations and it's important for programmers to be fluent in a wide variety of them and good at interfacing between different languages. But I'm increasingly coming to believe that good general-purpose languages are possible and that better systems are built in a single language, by programmers specialized to that language.
[1]: Called that because it is the problem of checking whether a given program is a satisfying theory -- i.e. a model -- for the given logical property.
Are there examples of cases where a system was very hard to verify with any one general technique, but much more practical to verify by using several domain-specific techniques and some kind of bridge between them (i.e. not simply coming up with a general approach for which the specialized techniques were, well, specializations - since as far as I can tell your quote is advocating for something different)?
I'm not sure what you mean by bridge but the halting problem comes to mind: the general case is impossible but you can prove common algorithms halt by showing they're structurally recursive (the recursive parameter always get smaller) or some metric always decreases on the recursive call (e.g. the sum of the length of two lists always gets smaller on the recursive call).
Right, but those are just special cases of the same technique - you can combined them by using dependent types to lift the list length to the type level and then this metric technique is just a special case of structural recursion.
Using dependent types is more of a particular notation than a solution to verification. How you prove your type inference/checking is the hard part. Examples of approaches include SAT/SMT solvers, symbolic model checking, manual deduction, explicit model checking, abstract interpretation (which is really abstraction + explicit model checking; H-M inference algorithms can be described in terms of this approach), weakest preconditions, etc. You can use all of these approaches to infer/check dependent types, just as you can use them to verify program logic stated using means other than dependent types.
Yes, because once you're representing the values with dependent types, metric recursion and structural recursion are physically the same thing.
For what it's worth, every time I see articles and comments about the use of formal verification in general purpose programming around here, I never see any mention of how the actual verification part requires incredibly challenging manual proofs. In particular, I see articles about dependent types that give the impression you get the proofs for free when that isn't the case.
> Even if "NSB" were universally seen as pessimistic, what is wrong with that? Is Einstein's statement that nothing can travel faster than the speed of light "bleak" or "gloomy?" How about Godel's result that some things cannot be computed? "NSB" undertakes to establish that "the very nature of software makes it unlikely that there will ever be any silver bullets." Turski, in his excellent response paper at the IFIP Conference, said eloquently:
>> Of all misguided scientific endeavours, none are more pathetic than the search for the philosophers' stone, a substance supposed to change base metals into gold. The supreme object of alchemy, ardently pursued by generations of researchers generously funded by secular and spiritual rulers, is an undiluted extract of wishful thinking, of the common assumption that things are as we would like them to be. It is a very human belief. It takes a lot of effort to accept the existence of insoluble problems. The wish to see a way out, against all odds, even when it is proven that it does not exist, is very, very strong. And most of us have a lot of sympathy for these courageous souls who try to achieve the impossible. And so it continues. Dissertations on squaring a circle are being written. Lotions to restore lost hair are concocted and sell well. Methods to improve software productivity are hatched and sell very well. All too often we are inclined to follow our own optimism (or exploit the optimistic hopes of our sponsors). All too often we are willing to disregard the voice of reason and heed the siren calls of panacea pushers.
> Turski and I both insist that pipe-dreaming inhibits forward progress and wastes effort.
> So we come back to fundamentals. Complexity is the business we are in, and complexity is what limits us. R. L. Glass, writing in 1988, accurately summarizes my 1995 views:
>> So what, in retrospect, have Parnas and Brooks said to us? That software development is a conceptually tough business. That magic solutions are not just around the corner. That it is timefor the practitioner to examine evolutionary improvements rather than to wait—or hope—for revolutionary ones.
>> Some in the software field find this to be a discouraging picture. They are the ones who still thought breakthroughs were near at hand.
>> But some of us—those of us crusty enough to think that we are realists—see this as a breath of fresh air. At last, we can focus on something a little more viable than pie in the sky. Now, perhaps, we can get on with the incremental improvements to software productivity that are possible, rather than waiting for the breakthroughs that are not likely to ever come.
---
So discussing some methods of formal verification (such as manually checking dependent types) as a solution is like saying a particle accelerator is the solution to the alchemist's problem. Theoretically it can work; in practice, it's often too much effort :)
Personally I'm not sure pipe-dreams inhibit forward progress, but they sure do generate a lot of noise...
Have you done any formal proofs before? You're severely underestimating how difficult and time consuming they are to do even if you do have some intuition about why they are correct. The sel4 microkernel took around 5 years for around 20 experts to verify for example. Verifying a program can result in you having to prove arbitrarily difficult maths theorems so it's similar to saying automating arbitrarily difficult maths theorems should be trivial.
> I think for most real-world code, the theorem that the code represents (in a Curry-Howard sense) tends to be trivial.
Yes, the theorem/specification statement may be trivial compared to the code but the hard part is coming up with the proof that shows the code matches the specification. You don't get this for free.
But you wouldn't write a program that depended on a theorem that wasn't proven, no? I mean often the only mathematically hard parts of a given program are in the libraries it uses - which could ship with their own proofs.
> Yes, the theorem/specification statement may be trivial compared to the code but the hard part is coming up with the proof that shows the code matches the specification. You don't get this for free.
Doesn't the structure of the code tell you how to structure the proof though? Like, if you've written code that appends to a list by appending a single element and recursing, the way you prove it correct is to prove that it appends a single element and that it recurses correctly. If you've written something that's supposed to be a sorting algorithm and the code rearranges the elements of a list, why is it that you believe this particular rearrangement of the elements is a correct sort? Isn't the answer to that question your proof of correctness?
If that were the case then we'd never have bugs :) The number of corner cases can be staggering. So the answer to "why do you believe a sorting algorithm sorts?" is "because I considered a few cases, in the hope that it's enough". Whether or not it actually is enough is the source of all bugs.
Just take a look at the state-space visualizations of real but positively tiny programs to understand how complex tiny, useful programs are: https://www3.hhu.de/stups/prob/index.php/State_space_visuali... Some seem structured enough (those are the toy examples), but some are far from it.
Or at this program that is known to never throw an exception, yet proving it is... hard:
Does this seem like an arbitrarily difficult math theorem (because it is)? See those two lines in the middle of `bar` where the result depends on the depth of the recursion (or loop)? That's what makes the proof incredibly hard, and it is very common in real world programs. Does the structure of the code suggest a proof?Writing this program in Idris and proving that the type of `foo` is `Int` rather than `Maybe Int` is equivalent to proving Goldbach's conjecture.
True, most functions don't look like this, but in pretty much every serious project I've seen, there were at least a couple of instances of code that is even more complicated.
Now, the real question is where do the expensive bugs lie. In code that's hard to prove or in code that's easy to prove (or equally in both)? That is a question that is certainly worth investigating. But wherever the expensive bugs lie, it's likely not in implementations of list append...
Not my experience, but shrug.
> Does the structure of the code suggest a proof?
No - but it does look like bad code.
> True, most functions don't look like this, but in pretty much every serious project I've seen, there were at least a couple of instances of code that is even more complicated.
I've seen code that looks like that, but it's always been easy enough to clear up. As my career goes on I'm starting to think that almost all real-world code is trivial.
> Now, the real question is where do the expensive bugs lie. In code that's hard to prove or in code that's easy to prove (or equally in both)?
My experience is that most production bugs are stupidly obvious things. And that possibly all bugs are either stupid "why doesn't the compiler catch that" cases, or code that is bad (unreadable) on its face. Possibly that's a tautology.
> But wherever the expensive bugs lie, it's likely not in implementations of list append...
You say that, but verification of JDK sorting uncovered a real bug.
We're working in very different worlds, then. Sure, maybe in CRUD webapps almost all code is trivial, but if it's trivial then bugs aren't that tricky anyway. But the code that runs distributed database clusters, or avionics software, is far from trivial, and we know (from years of software verification) that verifying that code is essentially hard.
> My experience is that most production bugs are stupidly obvious things. And that possibly all bugs are either stupid "why doesn't the compiler catch that" cases, or code that is bad (unreadable) on its face.
In that case you would see much bigger productivity differences between languages like Haskell and languages like Python, while most (admittedly scarce) data shows that the differences are tiny.
> but verification of JDK sorting uncovered a real bug.
That is a very complicated sorting algorithm, and uncovering it wasn't done automatically, but required hard work. It is precisely an example of small code that is complex, and while formal verification is possible (because it's small), it is not trivial and not automatic. In any event, that code had more to do with my Goldbach example and much less to do with list append. Proving it was nowhere near as trivial as proving append.
My cynical hypothesis would be that Haskell really does lower the defect rate by an order of magnitude or more in comparison to Python (in terms of e.g. correct handling of edge cases), but this doesn't noticeably impact productivity/business value for many use cases.
Proofs for nontrivial programs quickly get into undecidable areas in terms of proof automation. You might have relevant theorems lying around but how you combine them to create your proof is an undecidable problem.
As an example, if you have integer theorem statement where you can only multiply variables by constants (e.g. x * 5 + y * 2 ... = x * 2 + ...) there's an algorithm that can always find a proof. If you relax this restriction, no such algorithm does or can exist that will always find a proof.
> Doesn't the structure of the code tell you how to structure the proof though? Like, if you've written code that appends to a list by appending a single element and recursing, the way you prove it correct is to prove that it appends a single element and that it recurses correctly.
Usually you'd use inductive proofs to write those kinds of proofs and the induction scheme you use would follow the way recursion is done in the program. That doesn't mean the gaps in the proofs (e.g. base and step case) are trivial though.
> If you've written something that's supposed to be a sorting algorithm and the code rearranges the elements of a list, why is it that you believe this particular rearrangement of the elements is a correct sort? Isn't the answer to that question your proof of correctness?
The jump from a rough intuition about why something is provable to a proof is much larger than you'd think. I'd recommend following a tutorial on Coq. It's worthwhile even if you don't go beyond a quick look so you can appreciate the almost vertical learning curve if you're not well versed in maths and logic (which most programmers aren't) and how proving simple facts rigorously (e.g. "list_reverse (list_reverse x) = x") requires a lot of effort.
In the safety-critical software world, you see projects using model checkers to verify individual modules and deductive proofs (say, in Isabelle) to verify the interaction among modules or vice-versa. In the less-safety-critical software world, you see people commonly use static analyzers (employing abstract interpretation), even though those can only verify certain properties, because both interactive deductive proof and automatic model checking are too cost prohibitive.
But the problem in general is this: we are not at a point where any single approach nor a combination of several lets us fully verify a real-world program even of moderate side at any acceptable cost. I don't believe any moderately-sized program has ever been fully verified using any technique.
Sure. Which means I think we simply don't know enough to say one way or the other what kind of approach we will need for effective proofs. Maybe we will need to combine multiple techniques and have bridges between them. But maybe we really will be able to extend one particular technique to cover all the important cases, or find a single general approach that recovers all the useful techniques we've found so far as special cases.
Not true. We know that we cannot create a Turing-complete language with that property. We haven't proven that we'll never be able to create a general-purpose non-Turing-complete language. I might argue that Idris is already an example of such a thing.
Well, if you're referring to total languages, then they are Turing complete for all intents and purposes.
Total languages are not immune to the halting problem (or, rather, to its finite generalizations known as "bounded halting"). The classical formulation of the halting problem simply tells you that verifying a program in general is undecidable. But this is simply because a Turing machine is a finite structure that can describe an infinite one. So in some way, the halting problem is undecidable in the same way that finding the maximum or sorting an infinite list doesn't terminate. Yet once the list is finite (or the Turing machine is known to terminate), you then need to ask yourself how hard is it to find the maximum element in a finite list, how hard is it to sort it, and how hard is it to verify a program that is known to terminate? The answers to all these questions are well known, and quite different from one another. Finding the maximum takes Ω(n) (worst-case), sorting is Ω(n lg n), and verification is Ω(|S|), namely at least linear in the number of states the program takes until it terminates (this directly follows from a trivial generalization of the halting problem called "bounded halting"). So sure, total programs are known to terminate, and all we have left to do now to prove them correct is to overcome a super-exponential lower complexity bound... In practice that is just as undecidable as for programs that are not proven to terminate.
And, BTW, the lower complexity bounds for verification of finite state machines written in expressive languages is already PSPACE-complete. There cannot be a useful general programming language with verification bounds that are less than exponential (unless, that is, PSPACE=P); but that is a good thing: verification of total-functional programs is super-exponential. So my point is that even completely general verification of freakin' finite state machines is out of our reach in large-enough programs. It's doubtful you can find a useful computational model that's simpler.
Also, notice that any program could trivially be made total without changing its semantics. Give me a program you want verified, I'll add a decreasing counter starting with 10100 to all its loops/recursions, and now your program is total and you'll never know the difference. Does that make it any easier to verify?
The total-language people know this. They don't claim that this makes practical program verification any easier. In fact, the motivation for totality has nothing to do with program verification but with using C-H to prove general mathematical theorems. Non-termination, as you know, is the same as inconsistencies in those proofs (although not in proofs about programs; non-termination introduces no inconsistency to those). However, some people who are only familiar with the classical formulation of the halting theorem have concluded that totality => no halting problem => verification is possible! This is false, and was abundantly clear even in the 50s. Kurt Gödel, in a letter to von Neumann in 1956, mentions in passing this finite (and obvious) generalization of the halting theorem before raising (for the first time!) the question of P vs. NP.
Which of course remains an open question.
> even completely general verification of freakin' finite state machines is out of our reach in large-enough programs. It's doubtful you can find a useful computational model that's simpler.
Eh, maybe. I find it very hard to reason about finite state machines in programs as a human, so it doesn't surprise me that proving correctness properties about them would be hard. I'm not at all convinced that a general-purpose programming language necessarily includes support for fully general finite state machines.
> Also, notice that any program could trivially be made total without changing its semantics. Give me a program you want verified, I'll add a decreasing counter starting with 10100 to all its loops/recursions, and now your program is total and you'll never know the difference. Does that make it any easier to verify?
Yes - it eliminates the class of errors where one has "implemented" something by an infinite loop. It helps for concrete programs in the same way that it helps for theorems, no?
Technically yes, but as Scott Aaronson says, a universe where P=NP would probably look very different from ours (and PSPACE is harder than NP). In any event, verifying effectively Turing-complete languages (even total ones) is much harder than EXPTIME (and we know that EXPTIME > P).
> I find it very hard to reason about finite state machines in programs as a human
I didn't mean it like that (programming with explicit states). Just a model of computation where the number of states is bounded. Any program with finite memory is a finite state machine. Every language must support at least that.
> it eliminates the class of errors where one has "implemented" something by an infinite loop. It helps for concrete programs in the same way that it helps for theorems, no?
No, because when you prove a program property A you know that you've really proven "A or no-termination". So being able to prove any property is not an inconsistency. This is not the case for mathematical theorems that don't have running time, and where "no termination" is meaningless. If running time is 0, then A just means A, and if A is a contradiction then you have a real problem.
Now, what about eliminating non-termination from programs? Well, you're not really doing that either, because as far as we're concerned, a program that takes 10^100 steps doesn't really terminate at all. One could claim that people are more likely to accidentally write a function that loops forever than one that loops 2^64 times. This may be true, but this again relies on empirical facts rather than general mathematical properties.
In any case, what makes you think that languages like Idris may make verification easy? The few cases of programs verified in this mostly-manual way took years to prove, even for very small and intentionally "dumbed down" code.
Any program is (or can be modeled as) a finite state machine, sure. But useful programs are a small subset of the space of possible finite state machines. It's not beyond hope that we could find a subset that allowed us to write most useful programs but was easier to reason about.
> One could claim that people are more likely to accidentally write a function that loops forever than one that loops 2^64 times. This may be true, but this again relies on empirical facts rather than general mathematical properties.
I am worried about not-terminating-in-reasonable-time (though much less worried than I am about looping forever), but can't we just make that one of the properties we keep track of and prove with the same tools?
> In any case, what makes you think that languages like Idris may make verification easy? The few cases of programs verified in this mostly-manual way took years to prove, even for very small and intentionally "dumbed down" code.
I guess my experience that keeping track of more properties in the type system doesn't make coding any harder. Compare Rust - writing Rust programs essentially means proving that things have valid lifecycles and are not used outside of them. This is a complex property that mainstream programmers were not previously proving at all - that many had despaired of ever being able to prove. And yet in practice people who write Rust find that not only can they do it, but the additional proof effort quickly becomes barely noticeable. Likewise with Idris you're proving termination in finite (though possibly unreasonable) time and once you get used to doing that it doesn't actually seem noticeably harder than not doing so. So I'm kind of hopeful that we can just keep improving the type systems used by mainstream programming languages until writing a program naturally includes proving the important properties of that program without even noticing.
It is beyond hope that we find a subset that's generally easier to reason about. Verifying one line programs of this sort:
is already NP-complete (SAT). Adding some loops that are of depth 2 makes it PSPACE-complete (TQBF, aka QSAT). I can't think of a useful programming language that doesn't have even small-constant-depth loops (which makes it finite state) and simple boolean algebra. Software verification is about verifying some subsets of programs that humans happen to write. It is categorically impossible to write a general-purpose language where all programs are easier to verify than PSPACE.> but can't we just make that one of the properties we keep track of and prove with the same tools?
Sure, with super-exponential complexity :) But again, this is in the worst case. We hope that humans usually write programs that are simpler.
> I guess my experience that keeping track of more properties in the type system doesn't make coding any harder.
If you mean H-M types as in Haskell, then the properties those types enforce are either trivial (i.e. true for all programs, e.g. function returns Int), or a result of a finite state machine (that's the proving strength of H-M types). You cannot prove even a single bit of a program's output that's a result of non-constant-depth recursion (there's a special case for recursion which is of depth that's a constant multiple of the input length, like `map`). If we take Haskell, you can replace each of your functions with constant-depth recursion (0 or 1 would suffice in virtually all circumstances) and the program will still typecheck yet will be completely wrong.
As for Rust's linear types, that is precisely what I'm talking about. A certain class of bugs (memory errors) that humans are known to make and that verifying with abstract interpretation is easy. That's what software verification aims to do. We cannot hope of proving general programs generally correct, regardless of the language they're written in.
BTW, thinking of type systems muddles understanding in this case, because type systems are just notation. The verification taking place in most sound type systems is abstract interpretation. Yes, we can find more important properties to verify with abstract interpretation, but it has been proven that some properties will forever elude abstraction.
The way abstract interpretation works is that it translates the program into an "abstract" program which is just a finite state machine, with the number of states equal to the number of concrete types, and running an exhaustive model checker on that; this means that the complexity of inferring this kind of types is Ω(|S|), namely, linear in the number of concrete types. As abstract types can multiply the number of concrete types, the inference can become exponential in the worst-case, but it usually doesn't. Once you introduce dependent types, the algorithm is still Ω(|S|) -- linear in the number of state, i.e. types -- but now the number of types is unbounded, and so the problem becomes undecidable.
> until writing a program naturally includes proving the important properties of that program without even noticing.
You're right, but this entirely depends on which properties are found to be important (and has little to do with type systems specifically; again, this is mostly notation[1]), and that, in turn, is rather empirical.
[1]: Not entirely, though, but mostly.
Eh. Again, I don't think we necessarily need arbitrary boolean algebra - something that's hard enough to reason about as a human - and may be able to capture the valuable use cases in a simpler model. Fundamentally if we have any hope of doing verification at all, surely we can characterize the constraints we need for verification and then push them back to the programming language level.
> If we take Haskell, you can replace each of your functions with constant-depth recursion (0 or 1 would suffice in virtually all circumstances) and the program will still typecheck yet will be completely wrong.
Could you expand on this / give an example? I don't think I follow. And I take it from what you're saying that this doesn't apply if we permit dependent types?
> BTW, thinking of type systems muddles understanding in this case, because type systems are just notation. The verification taking place in most sound type systems is abstract interpretation. Yes, we can find more important properties to verify with abstract interpretation, but it has been proven that some properties will forever elude abstraction.
Properties that are important for real-world programs? Abstract interpretation sounds very similar to how we reason about programs as humans. It just seems like to the extent that we understand how to do something at all we should be able to formalize that understanding.
If we're talking about using programs to address open questions - a best-effort at the travelling salesman problem, say - then I can see how you might end up with a program that had a pile of heuristics that seemed to work but with no concrete understanding of how or if it worked - except that even then you'd probably use a well-known, formally validated heuristic rather than using the program as a medium for mathematical research. I just think (empirically) it would be very rare as a business requirement to need to do something completely unproven, and therefore it might be possible to have a useful general-purpose programming language that didn't allow doing that.
That is not what the verification community is trying to do at all, because trying to find a language that is not even NP-complete to verify and is still generally is absolutely impossible (explanation later). What the verification community is trying to do is to come up with approaches that make it possible/easy to verify some code, which is hopefully the majority of code. As far as languages go, the hope is that a language can make some verification of some code easier than in other languages. A general-purpose language that is at least useful in some cases, and in which all programs are easily verifiable can only exist if P=NP. The reason is this: at best, you can hope that the proof of correctness is checkable in polynomial time. This puts it in NP. If constructing a proof of correctness is possible in polynomial time, so is coming up with the solution in the first place. Namely, such a language wouldn't even need to be programmed. It will be a constraint solver (that somehow is in P). SQL minus boolean expressions might be the best you could do. Possibly useful, but certainly not general-purpose.
> Properties that are important for real-world programs?
Yes, and they are quite common in distributed algorithms.
> It just seems like to the extent that we understand how to do something at all we should be able to formalize that understanding.
Yet we can't because when we reason about something we assume a certain regularity of the state-space, that is often wrong in practice. That link I showed you where there are visualizations of state spaces, shows the one for the CAN bus protocol. It is the most complicated example on that page, and it is the very real protocol used by different components in your car that need to communicate.
> I just think (empirically) it would be very rare as a business requirement to need to do something completely unproven
That depends a lot on what you do. If you design schedulers for OS kernels, concurrent data structures, or distributed algorithms you see that these difficult cases are the rule rather than the exception.
I work on concurrent and distributed algorithms, and I do formal verification (TLA+ is my current tool of choice) most day every day. TLA+ offers both a theorem prover (a la Isabelle/Coq/Agda) as well as a model checker. Manual deductive proofs are virtually never worth the trouble (that would take me years), and even with a model checker -- where you just press a button and if there's a bug, any bug, you get a full trace of the execution that led to the bug -- it's still a lot of work, because distributed algorithms are just essentially complex.
This is like saying we need to extend individual AI algorithms that can play chess, Go, poker, drive a car etc. to a single algorithm that can do all of these things.
Yes. And?
However, I think in the future we will increasingly consider programming models separately from the language used to express them, and in that sense there will be completely general programming languages. Powerful bases to create the models themselves as libraries and DSLs.
How many intricately specified software projects have failed because the spec bore no correlation to user needs?
If this algorithm is used to dispense some type of medication, and I enter 3.1 and it murders you with 10 grams of alprazolam... well.... the algorithm is still correct.
Nobody is saying the formal proof approach will find all bugs, just that it helps find more bugs compared to not using it. You could make the same argument with acceptance testing: unless you specifically tried 3.1 as the input during testing, it might not give you the output you expect. Formal proof can be complimentary to traditional automated tests and QA.
For any non-trivial code, no matter how much formal analysis you do, you don't trust it until it's been properly tested.
Lol!