5 ms·

Of course, proving things, that is, doing mathematics requires work. But at least it's work that produces a useful result, unlike carrying out computations with

Of course, proving things, that is, doing mathematics requires work. But at least it's work that produces a useful result, unlike carrying out computations without paying attention to their meaning. (By the way, this meaning always exists, even if you don't particularly care about it.) And the best moment to study the meaning of a computation, in the sense of minimizing the amount of long-term work, is as early as possible, which is exactly what types force you to do.

pron 10y ago
But this is now a programming discussion, not a computation discussion. Also, I don't think it's right to declare things "useful" only if they're useful to the particular problems you're trying to solve. BTW, any logical formalism forces you to pay attention to meaning; choosing to encode the logic in types has advantages and disadvantages, but it is not at all the only way to logically describe a program.
- catnaroek 10y ago
  > Also, I don't think it's right to declare things "useful" only if they're useful to the particular problems you're trying to solve. Pray tell, what's the use of a computation without paying attention to its meaning? My use case is simply “knowing the meaning as early as possible”, and there ought to be no discussion that this should be everyone else's use case as well. Nobody performs a computation without some sort of expectation about the relation between the inputs and the outputs. > BTW, any logical formalism forces you to pay attention to meaning I never said types are the only way. For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning.
  - pron 10y ago
    > Pray tell, what's the use of a computation without paying attention to its meaning? First, I don't think that the only way to assign meaning to computation is by formally assigning meaning to the syntactic components that comprise its program, as written in some human-readable language. Most of the relevant meaning is in human interpretation of the input and output or the sensors and actuators. Components' meaning may be stated informally. I am not aware that formal meaning is the only valid meaning. People wrote the software that landed men on the moon in assembly; that was pretty meaningful. I believe this is still the prevailing view in computer science. Second, you keep identifying the notion of computation with the notion of a program written by a person. The theory of computation, from its earliest days -- by Turing himself -- has studied computational phenomena in neural networks, genetics (Turing was a pioneer of both NNs and genetic algorithms) and quantum phenomena. Some of the greatest achievements in CS are not specifically related to software (I count at least 20% of all Turing awards). > For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning. Or TLA+, which makes types notoriously more difficult to use by comparison.
    - catnaroek 10y ago
      > First, I don't think that the only way to assign meaning to computation is by formally assigning meaning to the syntactic components that comprise its program, as written in some human-readable language. Please suggest alternatives - that actually work. > Most of the relevant meaning is in human interpretation of the input and output or the sensors and actuators. The relation between the input and the output. This can only be stated formally. > Components' meaning may be stated informally. That leads to disaster very quickly. > I am not aware that formal meaning is the only valid meaning. Well, I am. Too much nonsense has been said as a result of not formalizing things. > Second, you keep identifying the notion of computation with the notion of a program written by a person. No. Even if a computation “arises in nature” (which is just your way of looking at things, actual physical phenomena is what you can measure, plain and simple), the only way to make sense of it is to write a program that reproduces the computation. This is how scientific theories work. > Or TLA+, which makes types notoriously more difficult to use by comparison. Some type systems are more difficult to use than others, and the type theory community is definitely guilty of not paying enough attention to usability, but I don't see how model checking has a higher power/cost ratio than sensibly designed type systems. Which tool satisfies the following criteria? (0) Compositionality: you can understand a large system by studying its parts in isolation. (1) Handles higher-order constructs (first-class functions, objects) gracefully. (2) Stops you from saying nonsense as early as possible. I rest my case.
      - pron 10y ago
        > Please suggest alternatives - that actually work. AFAIK, the only languages that fully express the computational meaning formally with types are the dependently typed ones. AFAIK, there has been exactly one non-trivial real-world program written in such a language, and its author wasn't too pleased with the process (I'm referring to CompCert and Xavier Leroy). Every other program in every other languages has most of its meaning expressed informally, in the mind of the programmer. Unless you believe that no programs work, then nearly all programs that do express most of their meaning informally. > Too much nonsense has been said as a result of not formalizing things. Formalizing things doesn't imbue them with good sense. You can state plenty of nonsense formally. The only thing you're guaranteed is that it's consistent nonsense, and, as someone said on one of my favorite TV shows, "The sole virtue of the ineffectual is consistency". > Which tool satisfies the following criteria? ... TLA+, and far more elegantly and simply than any typed language you've seen.

pron 10y ago

But this is now a programming discussion, not a computation discussion. Also, I don't think it's right to declare things "useful" only if they're useful to the particular problems you're trying to solve. BTW, any logical formalism forces you to pay attention to meaning; choosing to encode the logic in types has advantages and disadvantages, but it is not at all the only way to logically describe a program.

catnaroek 10y ago
> Also, I don't think it's right to declare things "useful" only if they're useful to the particular problems you're trying to solve. Pray tell, what's the use of a computation without paying attention to its meaning? My use case is simply “knowing the meaning as early as possible”, and there ought to be no discussion that this should be everyone else's use case as well. Nobody performs a computation without some sort of expectation about the relation between the inputs and the outputs. > BTW, any logical formalism forces you to pay attention to meaning I never said types are the only way. For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning.
- pron 10y ago
  > Pray tell, what's the use of a computation without paying attention to its meaning? First, I don't think that the only way to assign meaning to computation is by formally assigning meaning to the syntactic components that comprise its program, as written in some human-readable language. Most of the relevant meaning is in human interpretation of the input and output or the sensors and actuators. Components' meaning may be stated informally. I am not aware that formal meaning is the only valid meaning. People wrote the software that landed men on the moon in assembly; that was pretty meaningful. I believe this is still the prevailing view in computer science. Second, you keep identifying the notion of computation with the notion of a program written by a person. The theory of computation, from its earliest days -- by Turing himself -- has studied computational phenomena in neural networks, genetics (Turing was a pioneer of both NNs and genetic algorithms) and quantum phenomena. Some of the greatest achievements in CS are not specifically related to software (I count at least 20% of all Turing awards). > For instance, you could use Hoare logic, but it's notoriously more difficult to use, precisely because it gives programs no a priori meaning. Or TLA+, which makes types notoriously more difficult to use by comparison.
  - catnaroek 10y ago
    > First, I don't think that the only way to assign meaning to computation is by formally assigning meaning to the syntactic components that comprise its program, as written in some human-readable language. Please suggest alternatives - that actually work. > Most of the relevant meaning is in human interpretation of the input and output or the sensors and actuators. The relation between the input and the output. This can only be stated formally. > Components' meaning may be stated informally. That leads to disaster very quickly. > I am not aware that formal meaning is the only valid meaning. Well, I am. Too much nonsense has been said as a result of not formalizing things. > Second, you keep identifying the notion of computation with the notion of a program written by a person. No. Even if a computation “arises in nature” (which is just your way of looking at things, actual physical phenomena is what you can measure, plain and simple), the only way to make sense of it is to write a program that reproduces the computation. This is how scientific theories work. > Or TLA+, which makes types notoriously more difficult to use by comparison. Some type systems are more difficult to use than others, and the type theory community is definitely guilty of not paying enough attention to usability, but I don't see how model checking has a higher power/cost ratio than sensibly designed type systems. Which tool satisfies the following criteria? (0) Compositionality: you can understand a large system by studying its parts in isolation. (1) Handles higher-order constructs (first-class functions, objects) gracefully. (2) Stops you from saying nonsense as early as possible. I rest my case.
    - pron 10y ago
      > Please suggest alternatives - that actually work. AFAIK, the only languages that fully express the computational meaning formally with types are the dependently typed ones. AFAIK, there has been exactly one non-trivial real-world program written in such a language, and its author wasn't too pleased with the process (I'm referring to CompCert and Xavier Leroy). Every other program in every other languages has most of its meaning expressed informally, in the mind of the programmer. Unless you believe that no programs work, then nearly all programs that do express most of their meaning informally. > Too much nonsense has been said as a result of not formalizing things. Formalizing things doesn't imbue them with good sense. You can state plenty of nonsense formally. The only thing you're guaranteed is that it's consistent nonsense, and, as someone said on one of my favorite TV shows, "The sole virtue of the ineffectual is consistency". > Which tool satisfies the following criteria? ... TLA+, and far more elegantly and simply than any typed language you've seen.