Hacker News Reader

Comment by seliopou | Hacker News Reader

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

View on HN

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.

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.

Google uses a lot C++.

They've done some Web things.

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.

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?

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.

C++ has polymorphism and templates.

If you have a lot of dynamic typing, you may want to look at C instead.

>I like types, but jeez, the vast majority of web systems over the last decade were written in dynamic languages

That's because the vast majority of web systems are glorified CRUD apps, the easiest kind of application one can make.

When it comes to the real hard backend parts (not just some queue handling of video conversion tasks for example, but things like search engines, social graph stores, programs for finding the cheapest air tickets, etc.), they're usually done in languages like Java, Scala, C++, Go, etc.

Heck, even as web front-ends got more evolved, people developed several typing systems to assist us (Flow, Typescript, etc) to solve that need, we got Go, Hack. Optional types are also landing in PHP and even in Python -- there's a consensus among many people about a need for such things. And Google wrote their more complex apps in a Java lib that could spat out Javascript IIRC (GWT).

As for the non CRUD apps, from PostgeSQL, Chrome, Office and Photoshop to Pixelmator, OmniPlan, Notepad++ and Scrivener, nobody writes those in dynamic languages (where nobody obviously means: some outliers being excepted). One might argue that those are few (they are not, they are merely "fewer" than web systems. Still millions of programmers work in that space), but the point remains: for developing harder apps, people opt to static languages.

They are not making a claim backed up by scientific evidence, but are rather stating a believable assumption that premises the work. PL is more about studying type theory than a it figuring out why it is useful (which dives into non science design anyways).

There is plenty of work in PL that covers why type theory is useful. Check out the classic paper by Philip Wadler called "Theorems for free" that covers some of the terrific benefits of parametric polymorphism.

There has also been a good amount of discussion generated by organizations such as Jane Street concerning the benefits of static typing and type inference in practice. Notably, the free documentation (that is completely coupled with the code) that you get when you design software that takes advantage of the type system.

Wadler's work is great, I've seen his talk on this many times (where he has the lambda shirt on), but it doesn't really cover "why it is useful" just "why it is inevitable".

Really, how would you scientifically show that parametric polymorphism is "useful?" "Useful" isn't a very empirical property, it isn't something you can reliably measure. In a scientific paper, you can't just say something like:

> When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck.

without justification! You have a citation, or perhaps it is something just accepted universally (which it isn't, of course). At the very least, you have to weaken the statement a bit...like:

> When it comes to maintaining and evolving these systems, the lack of explicit static typing is probably a bottleneck.

You can't talk in absolutes without evidence. But you know, the benefits of static typing are clear via anecdotal experience, we only really argue about whether or not the benefits balance out the disadvantages of static typing (and how those disadvantages can be mitigated, and if that is enough...). Again, in arguing about this we are firmly in the area of design and not science.

With regards to definitive benefit that's backed up by scientific study (rather than just anecdote)-- the UK's Ministry of Defense commissioned a study (IV&V) on the error rate of long-lived code comparing C code bases (static but not too strict) vs Ada (static and fairly strict). They presented their findings Ada-Europe 2001. There was about a 1 to 10 error ratio. They subset the Ada code into formally verified by SPARK code, and the error rate -- I kid you not -- dropped another order of magnitude. I'd assert based on that study static typing is definitively more reliable when your problem domain is set in stone [the operational semantics of flight, stock markets, power plants]. Of course that doesn't extend to any 'exploratory' computing where your domain isn't strictly (pardon the pun) defined.

RE: Parametric polymorphism being "useful" - a pedant like me would claim for it to be of use, one has to demonstrate one clear instance of PP being of use - trivial or not - after which PP gains the attribute "useful" ;)

This UK study is an anecdotal data point. It is not a controlled study, it is just comparing project A to project B that differ, among other thing in the languages they were written in (and probably much more!). It doesn't tell us very much for sure, but again adds to the anecdotes that can shape our judgement.

Of course, useful has a low bar, but it also has a magnitude (X is useful if it is used, it might not be very useful though).

Incidentally, stock markets have been big on Lisp and Smalltalk, two languages not known for static typing. It turns out that language X is always used in the stock market, where X is the latest hot language (Scala, Haskell, Clojure...).

Based on that study I would assert that tight static typing is more reliable than static typing that is full of holes.

It doesn't speak to strong dynamic versus strong static at all.

Speaking of holes, of course dynamic typing can have holes also: if an interpreter or compiler misses a type check, the consequences are that the wrong operation is applied to an object. The result is corruption, crashing.

The correctness and completeness of a type scheme is orthogonal to static versus dynamic.

Are these advanced theorem proving benefits obtainable with static typing alone, or does everything also have to be effect free ("purely funtional")?

Formally, everything has to be effect free; furthermore, everything has to be strict (the potential for any value to be "bottom" breaks things).

You can apply the same intuition and things mostly work, but there can be a few surprises.

These theorems are a huge part of the "if it compiles it must be correct" feeling that functional programming often provides.

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

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.

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.

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.

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.

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.

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

But testing ensures no such thing, considering that comprehensive testing across the entire space of possible inputs for a unit is infeasible in most cases. Part of the usefulness of static typing is to prevent us from having to negotiate that state space explosion head on by a priori ruling out vast swaths of potential inputs.

I think static typing and testing are much more complementary than you're giving them credit for.

> But testing ensures no such thing

Yes it does. Empirically.

>considering that comprehensive testing across the entire space of possible inputs for a unit is infeasible in most cases

Fortunately, it is also not necessary, as numerous studies have found.

>I think static typing and testing are much more complementary than you're giving them credit for.

I totally agree that they are complementary. I find static typing to be most useful as checked documentation (for which, unlike the safety aspects, there is actual empirical evidence). Also, it makes various optimizations easy/cheap/predictable, which I find highly valuable.

Finally, it does help a little bit with correctness, though far less than what many people claim.

However, it also has costs that are not insignificant, in slowing down exploratory programming, compile-time costs, brittleness of designs and often code expansion / productivity.

More importantly, it appears to harm compositionality/reuse, at least at our current level of understanding. Both Unix Pipes and Filters and the Web, arguably the most successful reuse mechanisms in the history of software, are dynamically and somewhat loosely typed. In addition, personal computing was invented in around 20KLOC using Smalltalk, a dynamically typed OO language.

> > But testing ensures no such thing

> Yes it does. Empirically.

Your claim was "Testing ensures that the knowledge is checked." And, yes, testing ensures that the knowledge is checked - by the test.

mrbrowning's claim is that "Static typing ensures that some sliver of that knowledge is explicit and checked." That's also true (despite your reply of "No"). And note mrbrowning's use of the word "explicit". Type knowledge is more explicit than a test. It ensures that this data structure is an instance of the specified type. A test proves that in this set of circumstances this data structure behaves the way we expect, which is a weaker proof.

> It ensures that this data structure is an instance of the specified type.

But downcasts are unsafe.

> >considering that comprehensive testing across the entire space of possible inputs for a unit is infeasible in most cases > > Fortunately, it is also not necessary, as numerous studies have found.

If you know something about how some function or module works and you check the right corner cases, the only way a bug could be hiding in some of the other input combinations is if it were deliberately planted in the form of extra code, like "if the inputs are specifically x, y and z, then misbehave such and such".

For instance if we know that a 32 bit adder is made up of bunch of full adders, there are certain bit patterns we can use which tell us that the adders are working properly individually, and that they are hooked up together right. We don't have to test every A + B = C triplet, blackbox style.

First,

> some sliver

Second, I for the most part agree with you in the ways that are relevant to the point you're trying to make. However, the knowledge/tool distinction is a vague (in that they may fall on a spectrum) and ambiguous (both words tend to be moving targets), which is why I chose the term instrument instead. Mathematics is a tool only in the sense that it is knowledge that is applied towards some benefit, e.g., efficiency. Also,

> Compare Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."

This is again "proof" in the day-to-day mathematical sense of a convincing argument, not in the formal sense for writing down an expression per line such that each line can be logically deduced from some preceding lines through the the use of axioms. A type checker is literally a search procedure through the space of derivation trees to find a formal proof that this term has this type.

> "proof" in the day-to-day mathematical sense of a convincing argument

IIRC, that is the most that a so-called "proof" can ever be. I remember reading Carl Friedrich von Weizsäcker's "Aufbau der Physik"[1] in my younger years, and being somewhat flabbergasted when he starts by justifying classical logic, which he needs to do because later he talks about quantum logic, which is different.

Up to that point, it had never occurred to me to justify logic empirically, but now I can't imagine naively accepting it. That means that empirical evidence always trumps. Everything. If we find logical rules that we assume violated in the real world, we have to deal with it, not deny reality. Just like we had to accept that other aspects of the world we held as self-evident were not just theoretically contingent, but actually turned out not to be true.

> not in the formal sense for writing down an expression per line

> such that each line can be logically deduced from some preceding

> lines through the the use of axioms.

Hmm...that's how we always did (simple) mathematical proofs: line-by-line, with axioms or theorems justifying the transformation from line to line. Last time I checked, so-called "machine-proofs" are definitely seen as different by mathematicians, yes, but they are less well-respected, not more so. Has this changed?

[1] http://www.amazon.de/Aufbau-Physik-Carl-Friedrich-Weizsäcker...

Actually, empirical observation depends on the correctness of basic logic, which must therefore precede it. You can't do experiments without having a logical framework that allows you to interpret their results. You can certainly find people who've convinced themselves that they need to empirically check math. i.e. check that 30x100 = 3x1000 by rearranging beans on their kitchen floor. I wouldn't hire anyone who did that to paint my bathroom, though.

That's the fallacy of uncritical rationalism. See Popper.

I prove mathematical properties purely for the sake of proving them. The fact that they have any bearing on the real world is a mildly interesting diversion. Given this frame of reference, empirical evidence almost never enters the picture when justifying a proof. Indeed, empirical evidence is necessarily finite, whilst even some of the most simple proofs reference the infinite.

> I prove mathematical properties purely for the sake of proving them

Good for you. I also think pure maths can be a fun diversion.

> The fact that they have any bearing on the real world is a mildly interesting diversion.

Well, computer "science" is primarily an engineering discipline. It is therefore primarily, if not entirely, about having bearing on the real world. (And even if it were a "science", which it largely isn't, that would still be the case).

> Given this frame of reference, empirical evidence almost never enters the picture when justifying a proof.

Given this frame of reference, your proof is of no relevance to software, which was exactly my point: yes, you can do these proofs, but they are largely irrelevant, and even if relevant always subsidiary to empirical evidence.

> Indeed, empirical evidence is necessarily finite, whilst even some of the most simple proofs reference the infinite.

How do you know that while these proofs reference the infinite, they are actually applicable to the infinite? The answer is: you don't and you can't. You can only assume that the proof mechanisms you use actually do not break down. Now I am certainly convinced (= I believe) that induction will continue to work for all N if I prove 1 and N -> N+1, but I have only empirical evidence for small N to justify that belief. And if we found an M where it didn't, what then?

And of course, there always have been (and probably always will be) "proofs" that were later shown not to be correct, just like physical "laws" that turned out not to be laws. All knowledge is contingent, especially all-quantified knowledge.

And I have to admit that I find the naive/rigid belief (it is no more than that) in the absolute power of proofs...charming :-)

> Well, computer "science" is primarily an engineering discipline.

I would say that software engineering was the engineering discipline, and computer science a mathematical discipline.

My point was that the proof itself is not subsidiary to empirical evidence, only its application is, and in my eyes, there is merit in the proof, free from its application to the "real world", for example as a lemma to another proof. Consider it a form of separation of concerns: whilst I prove a theorem, I am not concerned with how it mirrors the observable world, but in order to apply it, of course I must ensure that its assumptions can be reliably observed. In this way, our "beliefs" are limited and do not taint the logic of the proof itself.

> How do you know that while these proofs reference the infinite, they are actually applicable to the infinite?

Which brings us to your next point: I do not know, I simply believe it to be true because it is convenient to do so. My point is that this belief or its refutation does not affect the worthiness of the proof, only that of its application.

I actually do not believe in the absolute power of proof, I don't think it is something you can get away with believing once presented with all the facts. I hope I've explained myself better in this comment though: I don't think our views are as antipodal as it first seemed.

Type checking is a conservative analysis, and the type correctness of a program is undecidable. But you can still rely on the knowledge generated by your type checker without having to run your program. Among other things, this allows you to optimize your program automatically.

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

Reply on news.ycombinator.com