4 ms·
> The well-known results quoted in my post show that global correctness properties cannot be modularized, nor does anyone claim they can be. You are seriously
by fmap 10y ago
> The well-known results quoted in my post show that global correctness properties cannot be modularized, nor does anyone claim they can be.
You are seriously overselling these results. Here's one way to make termination proofs modular: Take the graph of your function (vertices for each value of the arguments, edges for recursive calls) and take its transitive closure. If you can cover the transitive closure with an arbitrary number of individually well-founded relations, the function terminates.
> Yes, this is what abstract interpretation does, and types carry it out. But not every property survives this state reduction (most of them don't).
The point of having contextual equivalence or a program logic is that every property you can express in your programming language/logic survives this state reduction.
> Like I wrote in the post, we know of specific, positively tiny programs, that are known to elude the power of math completely.
You give an example of a termination problem which is equivalent to the consistency of ZFC. Does the consistency of ZFC "elude the power of math"? It's certainly a very simple question, much easier to write down than the Turing machine in question.
> Programs are much more like the gravity equation -- made of small simple parts, that may become completely chaotic when combined -- than any mathematical theorem.
This applies to mathematics as well. You can write down simple sounding questions, like the Collatz conjecture you mention, which are actually extremely complicated. This is the point where complexity theory comes into the picture. For instance, I could generate random types in the calculus of constructions (random propositions) and ask if that type is inhabited (the proposition is provable). This is an undecidable problem and for complexity theoretic reason most instances (of a certain shape) will actually be hard.
The concepts in programming aren't inherently more complicated than the concepts in mathematics. If anything, there are plenty of natural concepts in mathematics which behave far more chaotically than anything in CS (look at a table of homotopy groups of spheres and tell me where that pattern comes from).
> Most of the things you mention that are relevant to global properties have so far failed to scale to real-world programs. Affordable proof of ordinary software's global correctness is no longer a goal and certainly not a promise of contemporary software verification.
It's very much the goal for PLT. :)
In practice, it's also very much in the future. Right now verifying large programs is possible for a team of experts with a lot of time and money. A lot of the work in the 21st century has been to scale these theoretical methods to real languages. Most of the really big verification projects of today were unthinkable a decade ago. A decade or two in the future it'll probably be routine and just another tool you use, similar to static analysis or unit tests.
Right now the infrarstructure is just not there yet, and that's one of the reasons why formal verification is so expensive. But there are no fundamental restrictions which would prevent us from verifying, say, the Linux kernel. Apart from it being way too expensive. If it was written in a reasonable languages, which encouraged programmers to develop truly sound abstractions it could be orders of magnitude less expensive, though...
- pron 10y ago> You are seriously overselling these results. Maybe. Maybe not. No one knows for sure, and no one has anything to suggest that the path forward is now clear. Those results provide good enough cause to believe that the problem is very hard. Empirical experience only strengthens the belief in that assumption (suggesting that we cannot easily find an easy-to-categorize subset of programs that is generally useful yet easier enough than the worst-case). > Here's one way to make termination proofs modular: Take the graph of your function (vertices for each value of the arguments, edges for recursive calls) and take its transitive closure. If you can cover the transitive closure with an arbitrary number of individually well-founded relations, the function terminates. Sure, that's how abstract interpretation works. But it doesn't always work, and proving termination says absolutely nothing about proving other properties. > Does the consistency of ZFC "elude the power of math"? Yes. > The point of having contextual equivalence or a program logic is that every property you can express in your programming language/logic survives this state reduction. Then those properties are weak or the reduction is hard. It's a simple consequence of bounded halting and the model checking results (also, I think I've seen Cousot give some simple examples of properties that cannot survive state reduction). In any event, even if you find properties that you can reduce in this way, the "model-checking isn't FPT" result, shows that you won't be able to combine them to prove global results (unless the local property happens to be all that's necessary). > Right now verifying large programs is possible for a team of experts with a lot of time and money. No large or even mid-sized program has ever been verified using PLT methods, no matter the size of the team or the effort. A medium sized business program is ~1MLOC. A large one is ~5-10MLOC. Programs that have been formally verified using PLT approaches are hardly within an order of magnitude from 100kLOC (from below, of course). It is also important to know that those verified programs don't employ arbitrary common algorithms, but only the simplest possible algorithms, for the purpose of verification. > It's very much the goal for PLT. :) What gives you that impression? My impression is that the goal is to verify important "kernels" for security or other crucial properties, at some acceptable cost given the small size and the great importance. Maybe some people hope that affordable whole-program verification would one day be possible (this is not unique to the PLT approach), but I don't think that's the current goal. > A decade or two in the future it'll probably be routine and just another tool you use, similar to static analysis or unit tests. I am not aware of a single researcher who believes that, but I'd like to know who does. > But there are no fundamental restrictions which would prevent us from verifying, say, the Linux kernel. Apart from it being way too expensive. I'm not sure what you mean by "apart from it being too expensive". A restriction that sets the complexity of that task at more than the lifespan of the universe would be a fundamental restriction. Anyway, there are no known ones, no. But it's like saying that there are no known fundamental restrictions that prevent us from proving P /= NP or the Goldbach conjecture, but stating confidently that either will be accomplished in some known timeframe is a whole other matter. > If it was written in a reasonable languages, which encouraged programmers to develop truly sound abstractions it could be orders of magnitude less expensive, though... We don't know that at all, and there are certainly no known results that suggest this may be the case. No one knows whether "good abstractions" make verification scalable. This may be what some people hope, but it is no more or less promising, and no more or less substantiated than the hope that, say, CEGAR model checkers would be able to verify the Linux kernel. Both are theoretically possible outcomes, both show some promise, but neither makes us confident that it will one day be so. If anything, my money is on CEGAR, or some combined approach where CEGAR would do most of the work.