Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

On Two Views of Computation in Computer Science

pressron.wordpress.com

Post reply on HN
Print view View original

161–170 of 191 posts

Re: On Two Views of Computation in Computer Science

#161

Post by pron »

tome wrote: post #159
pron wrote: post #157

Earlier quoted context omitted.

> and the former still writes to the common variable before the latter reads it. This is not true. At no point in your induction is it proven that it is always the last process that writes x before the first reads it, nor is it necessarily the case. > then at least one of the two following things must happen: This, too, is untrue. The events may occur in the precise opposite order. If this were true, then it would ha…

> But any proof or any other kind of verification not carried out or verified by a computer is not formal. Very suprised to hear this from someone who wrote this very article on the nature of computation!

It was an informal statement :) In any event I said deduction rules or a computer, by which I meant some tool that can reduce the rote effort, and that we can be sure is itself correct.

Re: On Two Views of Computation in Computer Science

#162

Post by pron »

catnaroek wrote: post #158
pron wrote: post #157

Earlier quoted context omitted.

> and the former still writes to the common variable before the latter reads it. This is not true. At no point in your induction is it proven that it is always the last process that writes x before the first reads it, nor is it necessarily the case. > then at least one of the two following things must happen: This, too, is untrue. The events may occur in the precise opposite order. If this were true, then it would ha…

> At no point in your induction is it proven that it is always the last process that writes x before the first reads it, nor is it necessarily the case. I didn't say anything about “the last process”, though. I just took a collection of M processes, with some valid interleaving, and inserted one more process, at whatever index j, displacing all pre-existing proceses j...M-1 one place to the right. >> then at least on…

> I didn't say anything about “the last process”, though

Of course. Sorry. For some reason my mind read i as N. It was late at night... I'm convinced the proof follows from your invariant, but the inductive step is a bit tricky, as i is not the same for every interleaving. My proof is simpler, as the invariant holds for -- and more importantly, maintained by -- every step made by the system, and there's no need to consider various interleavings. It also doesn't require induction on N.

> The formality comes from the use of explicitly given deduction rules, not from the use of a computer.

That's true and I said as much, but doing so is extremely laborious. Do you actually use natural deduction?

Re: On Two Views of Computation in Computer Science

#163

Post by catnaroek »

pron wrote: post #162
catnaroek wrote: post #158

Earlier quoted context omitted.

> At no point in your induction is it proven that it is always the last process that writes x before the first reads it, nor is it necessarily the case. I didn't say anything about “the last process”, though. I just took a collection of M processes, with some valid interleaving, and inserted one more process, at whatever index j, displacing all pre-existing proceses j...M-1 one place to the right. >> then at least on…

> I didn't say anything about “the last process”, though Of course. Sorry. For some reason my mind read i as N. It was late at night... I'm convinced the proof follows from your invariant, but the inductive step is a bit tricky, as i is not the same for every interleaving. My proof is simpler, as the invariant holds for -- and more importantly, maintained by -- every step made by the system, and there's no need to co…

> but the inductive step is a bit tricky, as i is not the same for every interleaving

Ah, the joys of nondeterminism! It gives “there exists” an, ahem, “interesting” meaning. This is why I only do imperative and concurrent programming when it's absolutely necessary (e.g., when no functional and deterministic program could be asymptotically as efficient).

> My proof is simpler, as the invariant holds for -- and more importantly, maintained by -- every step made by the system

My invariant is prettier. It doesn't need to be maintained “throughout the computation”, because it's a static assertion about the program: “regardless of the interleaving of operations, there exists some i such that...” Almost invariably, the program is a much simpler mathematical object than the computations it gives rise to. Dijkstra noted “that our intellectual powers are rather geared to master static relations and that our powers to visualize processes evolving in time are relatively poorly developed.” https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E...

> It also doesn't require induction on N.

Induction on the program counter is even harder! The inductive case of my proof doesn't even look at the entire computation: it looks at most at three processes at a time. It's literally less work than what you propose.

> Do you actually use natural deduction?

In the design of type systems, yes. If I want to prove something by hand, hell no. Natural deduction is much nicer to prove things about than it is to prove things in.

Re: On Two Views of Computation in Computer Science

#164

Post by pron »

catnaroek wrote: post #163
pron wrote: post #162

Earlier quoted context omitted.

> I didn't say anything about “the last process”, though Of course. Sorry. For some reason my mind read i as N. It was late at night... I'm convinced the proof follows from your invariant, but the inductive step is a bit tricky, as i is not the same for every interleaving. My proof is simpler, as the invariant holds for -- and more importantly, maintained by -- every step made by the system, and there's no need to co…

> but the inductive step is a bit tricky, as i is not the same for every interleaving Ah, the joys of nondeterminism! It gives “there exists” an, ahem, “interesting” meaning. This is why I only do imperative and concurrent programming when it's absolutely necessary (e.g., when no functional and deterministic program could be asymptotically as efficient). > My proof is simpler, as the invariant holds for -- and more i…

> Ah, the joys of nondeterminism!

In TLA+ nondeterminism is as natural and graceful as determinism (it's a matter of ∨ vs ∧), and the functional concepts of parameterization and function types are just special cases. Nondeterminism is what allows refinement relations. You have it whenever you have types, but the language you use just doesn't use the same words to describe it.

> because it's a static assertion about the program

Mine is as static and as global as yours (and has the benefit of being easily verifiable mechanically)! You're just not trained to see it. You've been told that concurrency and imperative constructs are "dynamic" and are hard to reason about. That's just because FP is bad at reasoning about them, and prefers syntactic decomposition. There is nothing dynamic about a proper, pure description of what to you seems a messy dynamic process. The entire program is just a single, pure semantically unambiguous first-order predicate.

I had a discussion about this with a PLT person once, and he kept asking how you prove static properties in TLA+. It took me a while to understand what he meant, as "static" vs. "dynamic" are necessary when you want to reason about syntax. In simple logic, there's just a single formula.

> Almost invariably, the program is a much simpler mathematical object than the computations it gives rise to

You don't reason about each computation, but about what you'd call the "program", which in TLA+ is called the algorithm, as not to unnecessarily confuse with ideas that are related to syntax. The algorithm is just a boolean predicate, and my proof is that that predicate implies another (which implies the property).

Now when I look at how FP people reason about code I wonder why they have to complicate things so much. Sequential, concurrent, parallel, nondeterministic, deterministic, algorithms, properties -- they can all be reduced to a single first-order predicate, with the simple implication relation proving anything you want to know about any of them (that the program satisfies a property or a "type", that the deterministic program is a refinement of the nondeterministic one, that the parallel program computes the same result as the sequential one, that the sequential program has a worst-case complexity of such-and0such), all with simple, familiar logic and semantics that fit on a single page.

Re: On Two Views of Computation in Computer Science

#165

Post by pron »

tome wrote: post #160
pron wrote: post #149

Earlier quoted context omitted.

> No, I'm not. I'm talking about math. Good. In that case, verifying that a program conforms to spec in the general case is of as much computational complexity no matter when it's carried out. This is proven and well known. For an overview, you can see my post here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-c... In short, the reason for that is that the every computational problem with a computable u…

There is still one glaring issue with your thesis that remains unresolved. Verification is hard. We all agree. But that is for the worst case . Alternatively we can say that it is hard to verify arbitrary programs. I am utterly unconvinced that it is hard to verify programs that are designed to be verified, and I am utterly unconvinced that it is hard to design programs to be verified. How should I convince myself th…

> How should I convince myself that it is hard either (1) to verify even programs that are specifically designed to be verified, or (2) to write such programs?

Didn't we discuss that issue on Reddit? Anyway, as the complexity of verification is proportional to the number of states. If you write the program from scratch, the number of states is dictated by your spec (as every computational problem, every function has an inherent computational complexity). Your spec can be arbitrarily hard.

Now, it's not a matter of worst-case. That writing and verifying arbitrary programs is the very same problem is easy to see: given a program A, and a property I wish to verify P, I then create a spec S = A ∧ P, i.e, the program you write must behave like this arbitrary program and satisfy P. So there is no difference between writing from scratch or verifying. Indeed, you can see that static analysis tools can often prove on arbitrary programs the very same properties that are enforced by type systems.

Of course, not every algorithm and property are worst-case, regardless of whether the program is being written or given. There are useful classes of programs/properties that are easier to verify, and the language can make useful restrictions. So far, examples that work well in practice are SPARK and SCADE. Each forbids memory allocation, including unrestricted stack growth.

Re: On Two Views of Computation in Computer Science

#166

Post by tome »

pron wrote: post #165
tome wrote: post #160

Earlier quoted context omitted.

There is still one glaring issue with your thesis that remains unresolved. Verification is hard. We all agree. But that is for the worst case . Alternatively we can say that it is hard to verify arbitrary programs. I am utterly unconvinced that it is hard to verify programs that are designed to be verified, and I am utterly unconvinced that it is hard to design programs to be verified. How should I convince myself th…

> How should I convince myself that it is hard either (1) to verify even programs that are specifically designed to be verified, or (2) to write such programs? Didn't we discuss that issue on Reddit? Anyway, as the complexity of verification is proportional to the number of states. If you write the program from scratch, the number of states is dictated by your spec (as every computational problem, every function has…

> That writing and verifying arbitrary programs is the very same problem is easy to see: given a program A, and a property I wish to verify P, I then create a spec S = A ∧ P, i.e, the program you write must behave like this arbitrary program and satisfy P. So there is no difference between writing from scratch or verifying.

I don't follow. What has A got to do with it? I am given a spec P. You claim that it's hard to write a program that satisfies P, pretty much regardless of what P is. I don't see how A is relevant at all.

Re: On Two Views of Computation in Computer Science

#167

Post by pron »

tome wrote: post #166
pron wrote: post #165

Earlier quoted context omitted.

> How should I convince myself that it is hard either (1) to verify even programs that are specifically designed to be verified, or (2) to write such programs? Didn't we discuss that issue on Reddit? Anyway, as the complexity of verification is proportional to the number of states. If you write the program from scratch, the number of states is dictated by your spec (as every computational problem, every function has…

> That writing and verifying arbitrary programs is the very same problem is easy to see: given a program A, and a property I wish to verify P, I then create a spec S = A ∧ P, i.e, the program you write must behave like this arbitrary program and satisfy P. So there is no difference between writing from scratch or verifying. I don't follow. What has A got to do with it? I am given a spec P. You claim that it's hard to…

Yes, but P can be arbitrarily hard to implement. This is hard for you to see, so I'm incorporating A into P just as an example of how we can make the spec hard. If it were easy to write programs that conform to arbitrary specifications, it would have been just as easy to verify arbitrary programs, because I can reduce the latter to the former by making the arbitrary program the spec of the new one.

If you want another example of how a spec can be hard, consider this one: "write a program that for every input n, an even integer greater than two, outputs the smaller of two primes whose sum is n". Do you think writing that program and proving it correct is any easier than verifying the 10-liner in my post?

Or even this: "write a program that sorts a list of integers". You know for a fact that that program has a minimal time complexity of O(n lg n). That complexity, in turn, partly determines how hard it will be proving the program correct. You know that it will be easier than "write a program that returns the first element of its input list", whose time complexity is O(1) (actually the difficulty of verification is more related to the space complexity, because the space complexity is a better approximation of the number of states the algorithm must have in order to solve the problem, unless the algorithm can be a pushdown automaton).

Re: On Two Views of Computation in Computer Science

#168

Post by catnaroek »

pron wrote: post #164
catnaroek wrote: post #163

Earlier quoted context omitted.

> but the inductive step is a bit tricky, as i is not the same for every interleaving Ah, the joys of nondeterminism! It gives “there exists” an, ahem, “interesting” meaning. This is why I only do imperative and concurrent programming when it's absolutely necessary (e.g., when no functional and deterministic program could be asymptotically as efficient). > My proof is simpler, as the invariant holds for -- and more i…

> Ah, the joys of nondeterminism! In TLA+ nondeterminism is as natural and graceful as determinism (it's a matter of ∨ vs ∧), and the functional concepts of parameterization and function types are just special cases. Nondeterminism is what allows refinement relations. You have it whenever you have types, but the language you use just doesn't use the same words to describe it. > because it's a static assertion about t…

> You've been told that concurrency and imperative constructs are "dynamic" and are hard to reason about. That's just because FP is bad at reasoning about them, and prefers syntactic decomposition.

The hard fact is that, while you can reason about purely functional programs using little more than high-school algebra, reasoning about imperative programs requires bringing in the heavy apparatus of logic right from the start, because imperative programs denote predicate transformers. Distinguishing a class of computations that can be expressed as functional programs is distinguishing a class of computations whose meaning can be established with simpler tools, and thus obviously a beneficial activity.

> There is nothing dynamic about a proper, pure description of what to you seems a messy dynamic process. The entire program is just a single, pure semantically unambiguous first-order predicate.

Last time I checked, imperative programs don't denote first-order predicates, but rather predicate transformers. Quite different things. A predicate transformer is a higher-order mathematical object that relates two (possibly first-order) predicates - a precondition and a postcondition.

> You don't reason about each computation, but about what you'd call the "program", which in TLA+ is called the algorithm, as not to unnecessarily confuse with ideas that are related to syntax.

Your use of induction on the program counter reveals that you're just using the program as a proxy for a class of computations.

> The algorithm is just a boolean predicate,

Um, no. Predicates don't express computation.

> and my proof is that that predicate implies another (which implies the property).

Would you have been able to produce your proof entirely by yourself? That is, unaided by a computer. I produced my proof using nothing other than my brain.

Re: On Two Views of Computation in Computer Science

#169

Post by tome »

pron wrote: post #167
tome wrote: post #166

Earlier quoted context omitted.

> That writing and verifying arbitrary programs is the very same problem is easy to see: given a program A, and a property I wish to verify P, I then create a spec S = A ∧ P, i.e, the program you write must behave like this arbitrary program and satisfy P. So there is no difference between writing from scratch or verifying. I don't follow. What has A got to do with it? I am given a spec P. You claim that it's hard to…

Yes, but P can be arbitrarily hard to implement. This is hard for you to see, so I'm incorporating A into P just as an example of how we can make the spec hard. If it were easy to write programs that conform to arbitrary specifications, it would have been just as easy to verify arbitrary programs, because I can reduce the latter to the former by making the arbitrary program the spec of the new one. If you want anothe…

Sure, I know that there are some specifications P that are hard to implement (and some that are impossible!). What's not clear to me is whether the specifications we care about implementing in practice are hard to implement.

Re: On Two Views of Computation in Computer Science

#170

Post by pron »

tome wrote: post #169
pron wrote: post #167

Earlier quoted context omitted.

Yes, but P can be arbitrarily hard to implement. This is hard for you to see, so I'm incorporating A into P just as an example of how we can make the spec hard. If it were easy to write programs that conform to arbitrary specifications, it would have been just as easy to verify arbitrary programs, because I can reduce the latter to the former by making the arbitrary program the spec of the new one. If you want anothe…

Sure, I know that there are some specifications P that are hard to implement (and some that are impossible!). What's not clear to me is whether the specifications we care about implementing in practice are hard to implement.

In practice it's obvious that they're hard! Look at the bugs people make and look at the effort required for seL4/CompCert (both are fairly simple systems).
Post reply on HN