4 ms·

> The typing is in your head, where it doesn't get in the way. If the typing's in your head, then why not write it down for the benefit of others? and for the

> The typing is in your head, where it doesn't get in the way. If the typing's in your head, then why not write it down for the benefit of others? and for the personal benefit of automation provided by the compiler? The answer is that for even the most basic systems, a model of its operation cannot be retained in a single person's working memory for even a moment, nevermind the duration of a incremental refactoring. People have trouble remembering phone numbers long enough to dial them. How are you supposed to remember the complex interactions of functions, libraries, and any state that they might be managing? This is by far the greatest fallacy and self-delusion that is propagated by scripters. Talk about an assertion with a ton of evidence against it.

deleted 11y ago
[deleted]
alextgordon 11y ago
The same argument would say that it's impossible to write mathematics papers without proof assistants (Coq, etc). Obviously that is bogus, mathematicians are not 'deluded' about their ability to check their work themselves. It's just a skill.
- cwzwarich 11y ago
  In the analogy between programming and theorem-proving, programs correspond to proofs. When mathematicians informally check a proof, they are usually judging whether a complete proof could be produced, not whether the presented proof is a complete correct proof. Programmers are not given the same affordance.
- asQuirreL 11y ago
  I feel like the analogy would be "writing mathematical proofs without writing down any of the propositions" (And indeed, the Curry-Howard correspondence lends credence to this). Writing down types for programs is not just useful because the computer can check them, but also because it commits what is in one's mind. What's more, type-checkers offer a lot more help in checking types than Coq does at proving mathematical propositions (There is a reason, after all, that one is an assistant, whereas the other is a checker), so, relatively speaking, writing a proof without Coq is not as hard as typing a program without a type-checker.
- seliopou 11y ago
  Not the case. The same argument does not apply because of the nature of mathematical, and to a certain extent scientific. All three--mathematics, science, and computing (programming)--are similar in that their primary currency is knowledge that can be concisely described and embodied in instruments (tools), either of which can then be used by others without too much of a concern for where that knowledge or instrument came from as long as there's a good instruction manual nearby. The knowledge and instruments are used to create more knowledge, which is embodied in more instruments, and the cycle continues on and on etc. The difference between computing and mathematics is the form that the knowledge and the instruments take. In mathematics, the concepts you're dealing with (or inventing, since I'm not a mathematical realist) are very clean and they stack well. You also have virtually no instruments to speak of. As a mathematician, it's not too common that you reduce your theories to practice. That's something that's left to the lesser sciences, such as computing. In computing, the relationship between between knowledge and instruments is that of identity. At the very least, the two are conflated in casual discussion. More concretely, the "knowledge" of computing is typically a model of some problem domain and the the instruments are software, which in turn manipulate the physical world (that's what your JavaScript is doing) in order to perform some task or measurement in service of solving some problem in your domain. So in mathematics, you have no correspondence between knowledge and instruments to do deal with. In computing, that's all you're dealing with except people are only really interested in the knowledge as its embodiment in the instruments. Static typing ensures that some sliver of that knowledge is explicit and checked. It doesn't mean it corresponds to the thing in your brain, but it does ensure that whatever's written down is embodied in your code. Mathematicians have no such constraints to deal with. They would if the proofs that they wrote were formal proofs, but they're not. Most, if not all, mathematicians know this. Most programmers, though, don't.
  - mpweiher 11y ago
    > Static typing ensures that some sliver of that knowledge is explicit and checked. No. Testing ensures that the knowledge is checked. As in: run experiments. Empirical evidence. Static typing only checks one set of assumptions against another set of assumptions. Don't get me wrong, this is better than nothing. But the only real check is actually running the code, getting empirical evidence. In every other engineering discipline, math is seen as a tool, simulations are cost saving measure because running experiments for everything is too expensive. Only in the discipline where gathering empirical evidence is actually generally cheaper than trying to prove things (with mostly dubious value) is there this odd notion that using math is superior to running the experiment. If flying planes or running wind tunnel tests were as quick and cheap as running computer simulations, there would be no more computer simulations in aviation. Compare Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."
mpweiher 11y ago
> If the typing's in your head, then why not write > it down for the benefit of others? Because writing it down gets in the way while you are exploring.
- andrewflnr 11y ago
  To elaborate, some of the typing in your head is based on inaccurate domain assumptions that you're only going to find out about when you have some sort-of-working code to play with. It may not be worth writing down for others until you have something you know is going to last the week, or the day.
woah 11y ago
I like types, but jeez, the vast majority of web systems over the last decade were written in dynamic languages. You're trying to claim absolute proof for a very subjective choice, and it sounds silly.
- vosper 11y ago
  The vast majority by count, perhaps, but if you took complexity of functionality into account I bet you'd find static languages (specifically Java and C#) take the win.
  - paulddraper 11y ago
    Google uses a lot C++. They've done some Web things.
    - kazinator 11y ago
      There can be an awful lot of dynamic typing hiding inside C++ code bases, by the way. C++ has very good support for dynamic typing. You can make C++ look almost like Javascript, if you want.
      - paulddraper 11y ago
        C++ has polymorphism and templates. If you have a lot of dynamic typing, you may want to look at C instead.
      - marvy 11y ago
        How on earth do you make C++ like JS? I'm no JavaScript programmer so correct me if I'm wrong, but I think this is legal: x = 5; x = "five"; How do you do that in C++? In C# they have the dynamic keyword, but C++? I guess boost has all sorts of magic, but... good support?
        kazinator 11y ago
        That can be easily made to work in C++95. x can be of a smart pointer type (let's call it "var") which acts as reference to an anyobject class instance, which comes in varieties like string_anyobject, integer_anyobject and so on. The smart pointer class can have a few assignment operators and conversion constructors for usage like var x = "lit"; or x = 5.
kazinator 11y ago
> If the typing's in your head, then why not write it down for the benefit of others? Because then it would be dumb typing with explicit declarations, not state-of-the-art inferred typing. Also, you shouldn't write down or say everything that pops into your head. Doing so can have inconvenient consequences.

deleted 11y ago

[deleted]

alextgordon 11y ago

The same argument would say that it's impossible to write mathematics papers without proof assistants (Coq, etc). Obviously that is bogus, mathematicians are not 'deluded' about their ability to check their work themselves. It's just a skill.

cwzwarich 11y ago
In the analogy between programming and theorem-proving, programs correspond to proofs. When mathematicians informally check a proof, they are usually judging whether a complete proof could be produced, not whether the presented proof is a complete correct proof. Programmers are not given the same affordance.
asQuirreL 11y ago
I feel like the analogy would be "writing mathematical proofs without writing down any of the propositions" (And indeed, the Curry-Howard correspondence lends credence to this). Writing down types for programs is not just useful because the computer can check them, but also because it commits what is in one's mind. What's more, type-checkers offer a lot more help in checking types than Coq does at proving mathematical propositions (There is a reason, after all, that one is an assistant, whereas the other is a checker), so, relatively speaking, writing a proof without Coq is not as hard as typing a program without a type-checker.
seliopou 11y ago
Not the case. The same argument does not apply because of the nature of mathematical, and to a certain extent scientific. All three--mathematics, science, and computing (programming)--are similar in that their primary currency is knowledge that can be concisely described and embodied in instruments (tools), either of which can then be used by others without too much of a concern for where that knowledge or instrument came from as long as there's a good instruction manual nearby. The knowledge and instruments are used to create more knowledge, which is embodied in more instruments, and the cycle continues on and on etc. The difference between computing and mathematics is the form that the knowledge and the instruments take. In mathematics, the concepts you're dealing with (or inventing, since I'm not a mathematical realist) are very clean and they stack well. You also have virtually no instruments to speak of. As a mathematician, it's not too common that you reduce your theories to practice. That's something that's left to the lesser sciences, such as computing. In computing, the relationship between between knowledge and instruments is that of identity. At the very least, the two are conflated in casual discussion. More concretely, the "knowledge" of computing is typically a model of some problem domain and the the instruments are software, which in turn manipulate the physical world (that's what your JavaScript is doing) in order to perform some task or measurement in service of solving some problem in your domain. So in mathematics, you have no correspondence between knowledge and instruments to do deal with. In computing, that's all you're dealing with except people are only really interested in the knowledge as its embodiment in the instruments. Static typing ensures that some sliver of that knowledge is explicit and checked. It doesn't mean it corresponds to the thing in your brain, but it does ensure that whatever's written down is embodied in your code. Mathematicians have no such constraints to deal with. They would if the proofs that they wrote were formal proofs, but they're not. Most, if not all, mathematicians know this. Most programmers, though, don't.
- mpweiher 11y ago
  > Static typing ensures that some sliver of that knowledge is explicit and checked. No. Testing ensures that the knowledge is checked. As in: run experiments. Empirical evidence. Static typing only checks one set of assumptions against another set of assumptions. Don't get me wrong, this is better than nothing. But the only real check is actually running the code, getting empirical evidence. In every other engineering discipline, math is seen as a tool, simulations are cost saving measure because running experiments for everything is too expensive. Only in the discipline where gathering empirical evidence is actually generally cheaper than trying to prove things (with mostly dubious value) is there this odd notion that using math is superior to running the experiment. If flying planes or running wind tunnel tests were as quick and cheap as running computer simulations, there would be no more computer simulations in aviation. Compare Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."

mpweiher 11y ago

> If the typing's in your head, then why not write > it down for the benefit of others? Because writing it down gets in the way while you are exploring.

andrewflnr 11y ago
To elaborate, some of the typing in your head is based on inaccurate domain assumptions that you're only going to find out about when you have some sort-of-working code to play with. It may not be worth writing down for others until you have something you know is going to last the week, or the day.

woah 11y ago

I like types, but jeez, the vast majority of web systems over the last decade were written in dynamic languages. You're trying to claim absolute proof for a very subjective choice, and it sounds silly.

vosper 11y ago
The vast majority by count, perhaps, but if you took complexity of functionality into account I bet you'd find static languages (specifically Java and C#) take the win.
- paulddraper 11y ago
  Google uses a lot C++. They've done some Web things.
  - kazinator 11y ago
    There can be an awful lot of dynamic typing hiding inside C++ code bases, by the way. C++ has very good support for dynamic typing. You can make C++ look almost like Javascript, if you want.
    - paulddraper 11y ago
      C++ has polymorphism and templates. If you have a lot of dynamic typing, you may want to look at C instead.
    - marvy 11y ago
      How on earth do you make C++ like JS? I'm no JavaScript programmer so correct me if I'm wrong, but I think this is legal: x = 5; x = "five"; How do you do that in C++? In C# they have the dynamic keyword, but C++? I guess boost has all sorts of magic, but... good support?
      - kazinator 11y ago
        That can be easily made to work in C++95. x can be of a smart pointer type (let's call it "var") which acts as reference to an anyobject class instance, which comes in varieties like string_anyobject, integer_anyobject and so on. The smart pointer class can have a few assignment operators and conversion constructors for usage like var x = "lit"; or x = 5.

kazinator 11y ago

> If the typing's in your head, then why not write it down for the benefit of others? Because then it would be dumb typing with explicit declarations, not state-of-the-art inferred typing. Also, you shouldn't write down or say everything that pops into your head. Doing so can have inconvenient consequences.