Re:Total Functional Programming [pdf]
by pron on Friday October 07, 2016 @09:52AM
(#12660640)
> In particular, disjunctive termination proofs can be shown to be sound through Ramsey's theorem, and I don't see how to formulate this as an adjunction at all.
I have no idea what you just said, but I believe you :)
> it depends on your abstractions being connected to the same kind of semantics.
I'm side-tracking, but "semantics" requires a language. Not all computations are expressed in a language, and AI applies even to those of them that are not.
> If there was an interesting problem which was provably independent of ZFC, people wouldn't just give up.
Again, this is not the point. Whatever logic you choose, there would be programs whose behavior you cannot predict.
> You don't have to look to programs to find questions which are apparently "beyond math".
Of course, but we're talking about programs, and no one can deny the role of programs in the history of mathematics as examples of things that are hard (or impossible) to reason about.
> All I'm saying is that based on the empirical evidence, this is false. There are plenty of modular proof techniques and all formal verification projects (in the ITP sector) that I'm aware of report the overhead of verification as a constant factor.
This is indeed the main point of debate, although I'm not insisting on "exponential". The theory says things can in be really expensive (exponential and more), and the question is whether real-world programs are contained in a subset that is entirely different -- easy to verify -- or that they are spread throughout and can turn out to be arbitrarily hard (close to the worst case). I don't think empirical evidence settles this question, and it certainly doesn't suggest real programs are easy to verify. It is also certainly true that some programs -- when kept small and very simple -- in some specific domains, under lab conditions, have turned out to be not so terrible to verify. As someone who practices formal methods almost every day, I will certainly not say that things are hopeless, but I don't think we're in a position to say that the solution is near. We really don't know enough.
As someone who uses formal methods to reason about very complex distributed and concurrent algorithms (although deductive proof would take far more resources and time than we can hope to spend), formal verification works well (although I and many others who do this in the industry are skeptical about deduction), but the problem is different from program verification.
> This seems like a sweet spot for most applications.
Oh, I have no argument with you there. I totally agree. Deductive methods for the small, sensitive core if automated methods don't work, and automated methods -- with various degrees of confidence -- for the rest. But this isn't the same as saying that PLT approaches have "solved verification".
> This is why I focus so much on program logics and PLT methods.
Have you given TLA+ a look? I think it covers exactly what you're looking for far better than any PLT solution I've ever seen, for many reasons (generality, simplicity, ease, tooling, elegance). I'm always amused when I see yet another academic paper about formulating something in Coq, that an "ordinary" engineer would do with no more than little thought within a month of first laying eyes on TLA+. Just today I watched this talk from ICFP: https://www.youtube.com/watch?v=caSOTjr1z18 It didn't really make me understand what HoTT is about, but it did make me realize that PLT has taken a wrong turn somewhere and seems to be falling into the rabbit hole of foundational logic, if so much thought is put into a "computation" that isn't even algorithmic (i.e., it has a computational complexity of 0, and serves not the program but the formalism). If I remember correctly, "older" typed languages that PLT people are fond of like SML, didn't even have this problem that now requires a new foundation for mathematics (I'm exaggerating, but I think that not by much).
------
This, BTW, is a Twitter conversation between PLT-verification people, one of whom has worked on seL4. The bottom line is that we should work on FM -- it works in many cases -- but certainly "dismiss illusions" about it:
I have no idea what you just said, but I believe you :)
> it depends on your abstractions being connected to the same kind of semantics.
I'm side-tracking, but "semantics" requires a language. Not all computations are expressed in a language, and AI applies even to those of them that are not.
> If there was an interesting problem which was provably independent of ZFC, people wouldn't just give up.
Again, this is not the point. Whatever logic you choose, there would be programs whose behavior you cannot predict.
> You don't have to look to programs to find questions which are apparently "beyond math".
Of course, but we're talking about programs, and no one can deny the role of programs in the history of mathematics as examples of things that are hard (or impossible) to reason about.
> All I'm saying is that based on the empirical evidence, this is false. There are plenty of modular proof techniques and all formal verification projects (in the ITP sector) that I'm aware of report the overhead of verification as a constant factor.
This is indeed the main point of debate, although I'm not insisting on "exponential". The theory says things can in be really expensive (exponential and more), and the question is whether real-world programs are contained in a subset that is entirely different -- easy to verify -- or that they are spread throughout and can turn out to be arbitrarily hard (close to the worst case). I don't think empirical evidence settles this question, and it certainly doesn't suggest real programs are easy to verify. It is also certainly true that some programs -- when kept small and very simple -- in some specific domains, under lab conditions, have turned out to be not so terrible to verify. As someone who practices formal methods almost every day, I will certainly not say that things are hopeless, but I don't think we're in a position to say that the solution is near. We really don't know enough.
As someone who uses formal methods to reason about very complex distributed and concurrent algorithms (although deductive proof would take far more resources and time than we can hope to spend), formal verification works well (although I and many others who do this in the industry are skeptical about deduction), but the problem is different from program verification.
> This seems like a sweet spot for most applications.
Oh, I have no argument with you there. I totally agree. Deductive methods for the small, sensitive core if automated methods don't work, and automated methods -- with various degrees of confidence -- for the rest. But this isn't the same as saying that PLT approaches have "solved verification".
> This is why I focus so much on program logics and PLT methods.
Have you given TLA+ a look? I think it covers exactly what you're looking for far better than any PLT solution I've ever seen, for many reasons (generality, simplicity, ease, tooling, elegance). I'm always amused when I see yet another academic paper about formulating something in Coq, that an "ordinary" engineer would do with no more than little thought within a month of first laying eyes on TLA+. Just today I watched this talk from ICFP: https://www.youtube.com/watch?v=caSOTjr1z18 It didn't really make me understand what HoTT is about, but it did make me realize that PLT has taken a wrong turn somewhere and seems to be falling into the rabbit hole of foundational logic, if so much thought is put into a "computation" that isn't even algorithmic (i.e., it has a computational complexity of 0, and serves not the program but the formalism). If I remember correctly, "older" typed languages that PLT people are fond of like SML, didn't even have this problem that now requires a new foundation for mathematics (I'm exaggerating, but I think that not by much).
------
This, BTW, is a Twitter conversation between PLT-verification people, one of whom has worked on seL4. The bottom line is that we should work on FM -- it works in many cases -- but certainly "dismiss illusions" about it:
https://twitter.com/jonsterling/status/755794232929955840
I have an idea… We should ban the use of the word “trust” in “program verification” / “formal methods” circles.
https://twitter.com/jonsterling/status/755794326123196416
Well, if you ask me, we should ban the entire field of “formal methods”. Such a complete waste of time! very sad.
https://twitter.com/jonsterling/status/755794588300812288
By “waste of time”, I mean it’s intractable and really gnarly. Lot of folks get interested in it b/c they like type systems, but anyone who
https://twitter.com/jonsterling/status/755794781511389184
…is serious in the field knows that beautiful type theories aren’t going to get it done. What’s needed there is pure muscle and endurance
https://twitter.com/jonsterling/status/755794833437036544
…to bang through millions of lines of incredibly gnarly isabelle or coq code.
https://twitter.com/kamatsu8/status/755795189172539392
@jonsterling True. On my more cynical days, I say the main contribution of our seL4 project is the effective use of cheap student labor.
https://twitter.com/jonsterling/status/755795291949760513
@kamatsu8 Sorry, btw, for being snarky and dismissive. I should not have said “ban” but rather “dismiss our illusions about”.
https://twitter.com/kamatsu8/status/755798589075361792
@copumpkin @jonsterling In general I'd say formal methods are probably worth investigating, but there isn't going to be a silver bullet that
https://twitter.com/kamatsu8/status/755798808232026113
@copumpkin @jonsterling makes it always worth doing, which many FM people pretend exists even though it's provably impossible
https://twitter.com/kamatsu8/status/755798899319726080
@copumpkin @jonsterling and it's always going to be at least a little bit unpleasant.