5 ms·

That code includes a proof of correctness. A stronger form of verification than tests.

• yogthos 7y ago
  Yes, and my point is that there is a large cost associated with having such a proof.
  • mcguire 7y ago
    What is the cost associated with not having such a proof?
    • keymone 7y ago
      Not that high apparently, as there is no conclusive evidence for it.
    • yogthos 7y ago
      https://news.ycombinator.com/item?id=20330727 https://news.ycombinator.com/item?id=20330727
  • the_af 7y ago
    Don't forget that you also pay hidden costs when you forgo static proofs. It may be that you need to write more explicit tests by hand, or that you pay for the lack of verification with increased run time errors in production.
    • yogthos 7y ago
      Sure, however nobody has been shown that one approach is more costly than the other in practice. The most recent research available is the replication of the large scale GitHub study [1]. The relative effects of language choice on code quality is less than 1%. The main finding is that language choice hardly matters at all. On the other hand, we can easily measure the effects of factors like sleep [2], overwork [3], and happiness [4] on code quality. If static typing was an actual factor, we’d see exactly the same kinds of effects. There’s nothing wrong with enjoying static typing, but there’s simply no evidence that it plays any role past personal preference. Different people solve problems in different ways, and have different pain points. It's entirely possible that each type discipline appeals to different mindsets. That is a value in itself. [1] https://arxiv.org/abs/1901.10220 https://arxiv.org/abs/1901.10220 [2] https://arxiv.org/pdf/1805.02544.pdf https://arxiv.org/pdf/1805.02544.pdf [3] http://web.archive.org/web/20090824001133/http://www.curt.org/pdf/156.pdf http://web.archive.org/web/20090824001133/http://www.curt.or... [4] http://neverworkintheory.org/2014/05/01/happy-sw-devs-solve-problems-better.html http://neverworkintheory.org/2014/05/01/happy-sw-devs-solve-...
      • the_af 7y ago
        I don't disagree with what you're saying. I understand there's no hard evidence static typing is correlated with code quality. All I'm saying is that if you forgo static checks to avoid "paying the cost" -- and I do agree they come with a cost -- all you're doing is paying the cost elsewhere. Remember all those people saying "I don't need static types, I just write lots of tests"? That's a cost [1]. Or "I don't need types, I've never had type errors"? That's also a cost, though a more insidious one: ignoring that some of the errors they did get could have been prevented with a use of types they just aren't familiar with. I'm not arguing that static typing/analysis leads to better quality. I'm arguing that people who don't want to pay its cost actually pay it elsewhere. To be honest, if pressed I would also argue that I wouldn't want a critical system with the potential to endanger lives to be written in a dynamically typed language. Then again, static types alone wouldn't be suitable either. ---- [1] I knew one guy who didn't write tests either. "I don't need tests because they are a waste of my time: I never make mistakes". Guess where he paid the cost? :P Even then, not even writing tests is also an acceptable tradeoff in some situations!
        • yogthos 7y ago
          Right, both approaches have their respective costs. That's why I think it comes down to the pain points you're willing to live with. And as you note, you're going to have to write spedification tests for any serious software regardless of the type discipline. And it's also worth noting that there are other tools available, such a runtime contracts as seen in Racket and Clojure. If you have a specification for what the code is supposed to be doing, and you do specification testing then you will have a high level of confidence regardless of the type discipline. The kinds of errors that will slip through in a dynamic language would necessarily be edge cases and undefined behaviors. These are typically the kinds of bugs that static typing can help you catch. On the other hand, dynamic typing facilitates features such as hot loading. Just last week my team had a production issue where the service we were using changed the API, and the team managing it didn't notify us. We were able to update the code that talks to the service via the REPL with zero downtime. This is something that would've been a much bigger issue if we had to take the whole system down.