How Did Software Get So Reliable Without Proof? (1996) [pdf]
gwern.net
gwern.net
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.
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.
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.
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!
> 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:
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;
}
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:
if (a && ~b || c || ~d && e ...)
crash()
> 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.
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.
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