True that, but were/are there alternatives? Difficult to say.
True that, but were/are there alternatives? Difficult to say.
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.
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.
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.
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.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.
If you are broadening what you mean by CH, then fair enough, but it's shifting the argument.
This, of course, is annoying for almost all communication, particularly when we want to use fuzzy, hard to define terms. Languages are useful because you can pretty heavily butcher the syntax, but still be understood. (And arguably, that fuzziness is what drives new thoughts.)