5 ms·

> Anyway, therefore it follows that if we calcify and ossify data structures and types, we kill the progress, not to mention fun. I don't think it's fun to shi

> Anyway, therefore it follows that if we calcify and ossify data structures and types, we kill the progress, not to mention fun. I don't think it's fun to ship bugs to customers. I think it's much more fun to have a pervasive, mandatory proof engine that shows that I don't create these bugs in my software. (since it's mandatory, I can also help my teammates use my code correctly even though they don't understand how it works!) I make better progress when I'm not creating preventable bugs. My customers have more fun too. > This is blown out of reasonable proportion by static type advocates. In a dynamic system, type is de facto a few bits of value in an object. So the above situation is just another value that is wrong. It's wrong in a way that's totally preventable ahead of time. I'd rather take the proof engine and never suffer this class of bug. It certainly doesn't catch every bug, but I'll take what I can get.

kazinator 11y ago
> shows that I don't create these bugs in my software. Unfortunately, it doesn't show you that you don't create other than these easy bugs in the code. > It's wrong in a way totally preventable ahead of time. That would be a more powerful argument if all else could be held equal, which it rarely is. > I'll take what I can get. Local greediness is not always rationally founded. Anyway, dynamic typing doesn't preclude the proof engine. Dynamic programs can be analyzed to predict situations of inconsistent use of type, so that you can be informed. However, that doesn't prevent them from being executed, and still having the type representations at run time to resolve the situation. That is to say, programs for which the proof engine positively identifies one or more type error can be run anyway, as well as those for which it says "undecided" (not proven free of type errors, but no errors confirmed). Dynamic typing doesn't mean "I don't want my program analyzed prior to it being run; do not inform me of any impending issue of type!".

kazinator 11y ago

> shows that I don't create these bugs in my software. Unfortunately, it doesn't show you that you don't create other than these easy bugs in the code. > It's wrong in a way totally preventable ahead of time. That would be a more powerful argument if all else could be held equal, which it rarely is. > I'll take what I can get. Local greediness is not always rationally founded. Anyway, dynamic typing doesn't preclude the proof engine. Dynamic programs can be analyzed to predict situations of inconsistent use of type, so that you can be informed. However, that doesn't prevent them from being executed, and still having the type representations at run time to resolve the situation. That is to say, programs for which the proof engine positively identifies one or more type error can be run anyway, as well as those for which it says "undecided" (not proven free of type errors, but no errors confirmed). Dynamic typing doesn't mean "I don't want my program analyzed prior to it being run; do not inform me of any impending issue of type!".