Comment by throwaway729 | Hacker News Reader

Comment by throwaway729 | Hacker News Reader

Parent Full thread

> In a sense, perhaps a certain degree of ‘artificiality’ is at the core of logic throughout history, as it operates at levels of abstraction that are at odds with ordinary language usage

Of course, you could say the exact same thing for programming languages (after all, what do programmers do if not "simply working with special symbols, not with ordinary words"? And isn't this the primary criticism of programming brought by people who find it distasteful -- that expressing their fuzzy intuitions in a precise enough manner for the computer feels like a pointless exercise in frustration?)

Really, the only difference between the proponents of mathematical logic over informal prose in the early 20th century and the proponents of programming languages over informal prose today is that computers obviate the problem with fuzzy thinking and fuzzier exposition. The philosopher or mathematician could hand-wave about their holes in their arguments, but the programmer can only hand-wave so much the uselessness of his unexecutable pseudo-code.

The golden standard would be a form of speech that is natural and ordinary, but also avoids misleading, omitting, and eliding essential details.

In other words, a language that is formal enough to be parsed, checked, and generated by a proof assistant program. But also natural enough to be read as if it's prose written by a native speaker of a natural language.

I'm of the opinion that such a golden standard does not exist, and so we're forever doomed to incremental improvement.

On a slightly orthogonal note, I think that not only can you think of programming languages this way, but that you should—programming languages and formal logics are ultimately instances of the same general idea. I've found this to be a consistent and powerful view for reasoning about programs, programming languages, proofs and logics in a uniform sort of way.

The Curry-Howard correspondence is an important idea that's a specific instance of this, showing a direct relationship between specific kinds of logic and specific kinds of typed programming languages, but I think it's useful to think about programming languages that don't correspond to well-studied logical systems in a similar way.

This helps explain why the study of programming languages—and especially programming language theory—isn't really about programming languages: it's more about abstraction and reasoning in general. It's deeper than you'd suspect from the name. I'd go so far as saying that programming language theory is less a theory of programming languages and more a general theory of computation from a language point of view, as compared to "normal" theoretical CS.

   programming languages and 
   formal logics are ultimately 
   instances of the same general 
   idea.

That's deeply questionable. The CH-correspondence breaks down as soon as you your computation includes non-termination, concurrency, timing, distribution etc. Classical logic doesn't really have wholly convincing CH-correspondences either.

It seems to me that constructive proofs are a special class of programs, and fall under the purview of programming language, but not the other way around.

The point is that they're both formal systems of reasoning, not that they have exactly the same properties. The techniques and abstractions from both PL and formal logic often generalize well to both.

Non-determinism, a key property of concurrent systems, doesn't generalise well to logic.

Non termination is modeled as false: a function that takes an A and never terminates has type A -> F, or ~A.

There's some connection between classical logics and concurrency, though it's hard to get at. You can use callcc to implement threads, and Getzen's classical sequent calculus has multiple conclusions.

Here is a PHD thesis that uses modal logic to model distributed code in a CH fashion: http://www.cs.cmu.edu/~tom7/papers/modal-types-for-mobile-co...

Classical logic is perfectly modeled with callcc, which has the type Peirce's Law, and allows one to write terms with the types of the law of excluded middle or Double Negation Elimination.

   Non termination is modeled as false:

That means the CH correspondence is not interesting. If all non-terminating processes are falsity, types say nothing whatsoever of interest (from a specifiation and verification point of view) about non-terminating computation.

The T. Murphy PhD doesn't deal with distribution because it lacks the key feature of distribution which is partial failure.

As far as I'm aware the work on modelling double negation by call/cc doesn't actually provide a 1-to-1 correspondence between programs and proofs. I've forgotten the details but I think only some programs come out being proofs.

> The CH-correspondence breaks down as soon as you your computation includes non-termination, concurrency, timing, distribution etc.

No it doesn't. Each of those features leads to a different logic. You can even reason about the composition of logics via category theory to see how various features interact with each other.

> Classical logic doesn't really have wholly convincing CH-correspondences either.

Sure it does, first class continuations: http://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf

I suppose you have the right to remain unconvinced.

   can even reason about the composition of logics

I'm not aware of a fully fledged approach to logical composition that tells me an interesting story about the combination of logics that arise in computation, I know that people work on this, but as far as I can see, this work is far from finished. Please point to papers if you know more than that.

    first class continuations

As far as I'm aware, Griffin's work, which was a stroke of genius, does not provide a 1-to-1 correspondence between classical proofs and programs. That's why even today, 1/4 of a century later, people work on CH for classical logic.

It's true that the CH approach to classical logic is by no means exhausted. I see this as a feature of classical logic's rich structure. In any case, I disagree that this is a break down of the CH correspondence. Analyzing the type theories related to classical logic demonstrates to me that the CH correspondence is a gift that keeps on giving.

The approach I have in mind about composition of logics is the theory of pseudodistributive laws: http://dl.acm.org/citation.cfm?id=2612113

It's kind of cutting edge and has only yet been applied to a few situations, but it seems to be the correct notion of composing type theoretic (and hence logical) structures in compatible ways. Another approach I like that is strictly logical is Nuel Belnap's display logic, which characterizes a ridiculously broad range of logics and proves a general cut elimination theorem for them. The relationship between the categorical approach and the display logic approach is not entirely clear yet.

In any case, the CH correspondence is a rich and very active area of research. Just because we haven't nailed it down exactly yet doesn't mean it's broken! Our current understanding is a shadow of a much deeper concept.

The essence of CH is "proofs = programs" and "program execution = cut elimination". As far as I understand this does not work precisely as of Jan 2017 for most forms of computation beyond strongly normalising pure functions.

If you are broadening what you mean by CH, then fair enough, but it's shifting the argument.

"Obviate" does not mean "make obvious", as I think was intended here. "To obviate" means "to remove (a need or difficulty)".

Reply on news.ycombinator.com