|
The most important thing to realize is that, if you can no longer feel comfortable with shipping code "that can fail in various scenarios" then you would need the tests anyway. TypeScript and Java are not Coq, and you probably wouldn't enjoy using a properly rigorous language like that anyway (and the kinds of programs that can actually be "statically proven correct" are generally not very capable). Type checking doesn't make e.g. the halting problem go away; you are only verifying that types are compatible and not that the code actually does what it's supposed to do. Anyway, when you write code in a dynamically typed language, you do work in a restricted domain - just implicitly. You expect the input to provide a particular interface, and if it doesn't, there will be some kind of runtime exception. Oh well. You use exceptions for runtime debugging, not just to detect user error. Yes, this does require a different sort of discipline. But there is no accounting for taste. The language you describe are not only statically typed, but manifestly typed - i.e., you need to explicitly specify types within the code. Some people like the visual reminder; others loathe the extra typing (er, keypresses). Of course there are also statically typed languages that infer typing from use patterns, such as the Haskell family. > I was not able to maintain few guarantees here like : if I take X = XS[0], there is no way for typescript to guarantee that X is a value is that is guaranteed to be contained in XS. Well, yes; membership in a container is not type information. It can't be, not for mutable containers anyway. After all, the contents are determined at runtime. |