4 ms·

> 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 w

> 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.

tikhonj 10y ago
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.
- mafribe 10y ago
  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.
  - tikhonj 10y ago
    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.
    - mafribe 10y ago
      Non-determinism, a key property of concurrent systems, doesn't generalise well to logic.
  - mkehrt 10y ago
    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-code.pdf 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.
    - mafribe 10y ago
      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.
okintheory 10y ago
"Obviate" does not mean "make obvious", as I think was intended here. "To obviate" means "to remove (a need or difficulty)".

tikhonj 10y ago

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.

mafribe 10y ago
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.
- tikhonj 10y ago
  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.
  - mafribe 10y ago
    Non-determinism, a key property of concurrent systems, doesn't generalise well to logic.
- mkehrt 10y ago
  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-code.pdf 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.
  - mafribe 10y ago
    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.

okintheory 10y ago

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