5 ms·

"The idea that ordinary language is expressively inadequate to account for mathematical (or even logical) reasoning became a recurring theme in the ensuing trad

by kensai 10y ago

"The idea that ordinary language is expressively inadequate to account for mathematical (or even logical) reasoning became a recurring theme in the ensuing tradition of mathematical logic, so much so that the term ‘symbolic logic’ became synonymous with this tradition. Doing logic came to mean simply working with special symbols, not with ordinary words. In this respect, it is worth noting that the humanist authors had criticised the Latin of scholastic logicians precisely as ‘too artificial’, and even the Greek language that Aristotle relies on for syllogistic logic is regimented and removed from ordinary ways of speaking at the time. 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." True that, but were/are there alternatives? Difficult to say.

throwaway729 10y ago
> 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.
SomeStupidPoint 10y ago
The whole drive of mathematics (and logic) is ultimately that syntax is the semantics. 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.)

by kensai 10y ago

throwaway729 10y ago

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

SomeStupidPoint 10y ago

The whole drive of mathematics (and logic) is ultimately that syntax is the semantics. 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.)