3 ms·

I guess that's why all those statically typed programs don't have any bugs and don't need any tests. Being "sound" just means you can prove things are consiste

I guess that's why all those statically typed programs don't have any bugs and don't need any tests. Being "sound" just means you can prove things are consistent with the assumptions you can encode in it. If there are things you can't encode in the types, or if your assumptions are wrong (misapprehension being one of the main problems in software), or if your requirements change, soundness is not going to save you. Static types and proofs are valuable. Programs like compilers have fixed inputs and outputs and are excellent places to lean on things you can prove. But most of the programs I've worked on are not like compilers. They run for years, the requirements change, they have to deal with dirty data, talk to other messy systems, etc. And I'm not saying that dynamic types are perfect either. My point is simply that static types are not a magical end goal of programming. They are a tool with tradeoffs.

hota_mazi 8y ago
> I guess that's why all those statically typed programs don't have any bugs and don't need any tests. This is both a straw man and a fallacy. Nicely done. Also something I never claimed. You are basically saying that since you can't prove a program can be 100% demonstrated to be correct, there's no point in trying to approach this goal, therefore dynamically typed languages are good enough. With your reasoning, we wouldn't be using safety belts because they can't guarantee you'll survive a car crash 100%. Sure, static types have trade offs, but they are a clear improvement on all dimensions over dynamic types, which is why we see dynamic languages converging toward static typing and never the other way around. In ten years from now, we'll look at dynamically typed languages as "It looked cool at the time, but we know better now". A bit like we look at FORTRAN and COBOL today.
- puredanger 8y ago
  > Sure, static types have trade offs, but they are a clear improvement on all dimensions over dynamic types That has not been my experience and I don't think there is much objective proof of this. Most of the (admittedly not great) studies I've seen show dynamic languages as comparing favorably or better in bug counts for example. Some of the things we're working on in the next version of spec are is head-on the notion of how to define expressive contracts for functions and allow those to meaningfully evolve in compatible ways over time as program requirements change. I look at FORTRAN as a great language for its domain, so maybe you're right. :)
- disconcision 8y ago
  > Sure, static types have trade offs, but they are a clear improvement on all dimensions over dynamic types This statement seems self-contradictory.

hota_mazi 8y ago

> I guess that's why all those statically typed programs don't have any bugs and don't need any tests. This is both a straw man and a fallacy. Nicely done. Also something I never claimed. You are basically saying that since you can't prove a program can be 100% demonstrated to be correct, there's no point in trying to approach this goal, therefore dynamically typed languages are good enough. With your reasoning, we wouldn't be using safety belts because they can't guarantee you'll survive a car crash 100%. Sure, static types have trade offs, but they are a clear improvement on all dimensions over dynamic types, which is why we see dynamic languages converging toward static typing and never the other way around. In ten years from now, we'll look at dynamically typed languages as "It looked cool at the time, but we know better now". A bit like we look at FORTRAN and COBOL today.

puredanger 8y ago
> Sure, static types have trade offs, but they are a clear improvement on all dimensions over dynamic types That has not been my experience and I don't think there is much objective proof of this. Most of the (admittedly not great) studies I've seen show dynamic languages as comparing favorably or better in bug counts for example. Some of the things we're working on in the next version of spec are is head-on the notion of how to define expressive contracts for functions and allow those to meaningfully evolve in compatible ways over time as program requirements change. I look at FORTRAN as a great language for its domain, so maybe you're right. :)
disconcision 8y ago
> Sure, static types have trade offs, but they are a clear improvement on all dimensions over dynamic types This statement seems self-contradictory.