35 ms·

I'm not addressing formal verification itself, but in the argument between dynamic languages and compiled type-checked languages, I haven't found the tradeoff a

I'm not addressing formal verification itself, but in the argument between dynamic languages and compiled type-checked languages, I haven't found the tradeoff as you describe. I also have 20+ years in development and consulting, and I'm someone equally skilled in dynamic languages (particularly php) and compiled languages (mostly java, with scala and FP concepts mixed in). My current long term project is something where I'm the sole person on the team capable of deeply understanding their two main sets of legacy code. Both have been in active development for around fifteen years. One is in php, and one is in java. Both have significant technical debt, with several efforts of "modernization" that have only touched parts of the codebases. At this point, adding new features to the php codebase is harder. There are weirder runtime problems. The codebase is more difficult to understand. The side effects of any new features in the php codebase are more difficult to predict. When developing features that have any hope of actually succeeding and sticking around for a while, the truth is that area of code is going to be read, analyzed, and understood (or attempted to be understood) far more often than it will be written. So any initial benefit you get in writing speed is more than swallowed up over time in its difficulty to re-read, understand, and maintain. After dealing with both approaches for several years, my opinion is pretty firmly set that the dynamic approach is best for prototyping, or for a quickly-written simple service that won't grow, or if you're perhaps a startup writing a demo and scrambling for your first rounds of funding. But if you're looking at business features of any complexity, want to maintain them over a significant period of time, through a significantly changing number of eyeballs, and making a significant number of changes while leaving the codebase somewhat understandable... over the long run, the typed codebase will be easier and faster. I think the problem is that with typed systems, the costs are more explicit, but with dynamic systems, the costs are embedded in decisions like "That feature sounds too hard for that codebase, let's not do it (and thereby cede ground to competitors)."

wellpast 7y ago
I don’t disagree with you about maintaining large unwieldy code bases being perhaps better in static type land. Large unwieldy code bases have already ossified anyway so the productivity gain of dynamism is lost and you’re simply swimming in complexity. But my argument is that what got you the large unwieldy code base is a lack of skill set that no type system could protect you from. With the right toolkit (which includes nominal static typing among many other tools) and expertise you are not being optimal by giving highest precedent to formal machine proof systems which is what strong static typing does.
- zozbot234 7y ago
  Properly used, static typing actually enhances modularity and reduces unwanted coupling among software components. This means that a larger code base is far less likely to become practically "unwieldly" if static types have been consistently used in development. Even in exploratory programming where dynamic types may actually have some limited value, using them effectively requires a lot more "skill".
  - wellpast 7y ago
    Thought experiment, in your mind what would better produce modularity — TDD or static type verification? If you had to pick one.
    - tome 7y ago
      Anecdata: in Python I used to (and still do to some extent) practice TDD very conscientiously because I felt it really helped me structure my programs well and get them "correct my construction". One of the reasons for moving to Haskell was that the type system has the same effect at a lower cost (once the barrier to entry of learning about the type system has been crossed).
dllthomas 7y ago
In my experience, it's very much about time; I find myself able to work faster in a typed setting. Given testimony such as yours (which is by no means unique), and the inability of studies to show either approach clearly wins, my takeaway is that this is very sensitive to what particular skills we bring to the table. Different people work differently. And to some degree that's okay. It behooves us all to try and understand what is working for those who choose different approaches, rather than just ranting about how blind they must be. (I don't always remember that, myself.)

wellpast 7y ago

I don’t disagree with you about maintaining large unwieldy code bases being perhaps better in static type land. Large unwieldy code bases have already ossified anyway so the productivity gain of dynamism is lost and you’re simply swimming in complexity. But my argument is that what got you the large unwieldy code base is a lack of skill set that no type system could protect you from. With the right toolkit (which includes nominal static typing among many other tools) and expertise you are not being optimal by giving highest precedent to formal machine proof systems which is what strong static typing does.

zozbot234 7y ago
Properly used, static typing actually enhances modularity and reduces unwanted coupling among software components. This means that a larger code base is far less likely to become practically "unwieldly" if static types have been consistently used in development. Even in exploratory programming where dynamic types may actually have some limited value, using them effectively requires a lot more "skill".
- wellpast 7y ago
  Thought experiment, in your mind what would better produce modularity — TDD or static type verification? If you had to pick one.
  - tome 7y ago
    Anecdata: in Python I used to (and still do to some extent) practice TDD very conscientiously because I felt it really helped me structure my programs well and get them "correct my construction". One of the reasons for moving to Haskell was that the type system has the same effect at a lower cost (once the barrier to entry of learning about the type system has been crossed).

dllthomas 7y ago

In my experience, it's very much about time; I find myself able to work faster in a typed setting. Given testimony such as yours (which is by no means unique), and the inability of studies to show either approach clearly wins, my takeaway is that this is very sensitive to what particular skills we bring to the table. Different people work differently. And to some degree that's okay. It behooves us all to try and understand what is working for those who choose different approaches, rather than just ranting about how blind they must be. (I don't always remember that, myself.)