5 ms·
I use a strongly, statically typed functional language. Because my code has no mutable state, the type system of the program proves the program correct. So I do
by lbarrow 13y ago
I use a strongly, statically typed functional language. Because my code has no mutable state, the type system of the program proves the program correct. So I don't have to write any tests at all and maintenance is easy.
- MichaelSalib 13y agoWhich type system proves program correctness? A good type system can guarantee that your program doesn't suffer from certain classes of errors but that's very very far from correctness. Unless you only write programs that don't have any goal at all besides being memory safe: Behold MemSafe 2.9: it doesn't do anything at all, and most importantly, it doesn't do it in a memory safe way!
- DanWaterworth 13y agoAll safe type systems provide proofs that implementations fulfil specifications, but most type systems aren't expressive enough to create interesting specifications. The notable exceptions being type systems in dependently typed languages.
- gizmo686 13y agoA strong type system can do more than prove memory safety. It can guarantee that their are no unhandled cases, and that data has been properly processed before going into a certain use; however it (generally) cannot guarantee correctness. I say generally because the Haskell type system (with some extensions) is Turing complete, so you probably code implement a code prover in the type system.
- PommeDeTerre 13y agoNow and then I get to deal with development groups who have built their software systems using a language like Ruby or PHP. Many of them are proud of their extensive automated tests. They'll brag about how they have 45,000 or more unit tests, for instance. Yet when we actually look at these tests, many of them just end up implementing a half-baked type system. Even if they don't realize it, or don't want to acknowledge it, users of dynamic languages do want strong, static typing. It is one of the most useful tools there is when it comes to helping detect or avoid various problems. Rather than doing it in a sensible matter, by letting the computer (via a compiler, for example) efficiently do the hard or tedious work, they just choose to do it themselves manually.
- icebraining 13y agoAs a Python programmer, I don't mind a type system that's actually useful and doesn't get in my way. Unfortunately, the most popular statically typed languages have shitty type systems. Maybe someday I'll learn Haskell and get a job writing in it, but until then, I'd rather keep my sanity.
- emiljbs 13y ago(define square ((a number)) :out number (+ a 2)) This program is arguably incorrect, even though the types match up and there is no mutable state.
- doublec 13y agoSome languages can detect this at compile time. For example, ATS - a dependently typed language: fun square {m:int} (a: int m): int (m*m) = a + 2 This won't compile because in the type we've said the result must be the square of the input. I've written some more about using dependent types [1] and proofs [2,3] for this sort of thing. The difference between writing proofs and writing tests is subtle though and serve similar purposes. Tests can make you feel confident that things are right but proofs should make you certain of it. [1] http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.html http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.h... [2] http://bluishcoder.co.nz/2013/07/01/constructing-proofs-with-dataprop-in-ats.html http://bluishcoder.co.nz/2013/07/01/constructing-proofs-with... [3] http://bluishcoder.co.nz/2012/10/04/implementing-a-stack-with-proofs-in-ats.html http://bluishcoder.co.nz/2012/10/04/implementing-a-stack-wit...
- lbarrow 13y agoThe program is correct, but the function name is wrong.
- mcmillion 13y agoNot sure if you're trolling or just don't understand what tests are actually supposed to test.
- DanWaterworth 13y agoI'll bite. What are tests supposed to test?
- icebraining 13y agoThat the code is doing what you wanted it to do, instead of what you actually wrote?
- DanWaterworth 13y agoWell, they fail miserably then.
- colanderman 13y agoAs someone who uses strongly, statically typed functional languages (dependent ones like Coq no less), and who rarely writes unit tests, I downvoted you because you're wrong. Specifically: > the type system of the program proves the program correct. Is not a valid statement, unless you're actually writing proofs in Coq. I bet you aren't. "The type system of the program proves many simple properties of the program correct" is much more correct. Also: > Because my code has no mutable state No, that's not why. The type system you use may be incapable of reasoning about mutable state, which coincidentally serves to indicate that it most likely can't reason about such things as "this list is sorted", further supporting my initial counterpoint. Check out ATS or Why for examples of languages that permit reasoning about mutable state.
- angersock 13y ago>> don't have to write any tests at all That is, until you find out that your state-machine matches incorrectly on an input text file... >> maintenance is easy. ...and you are the only person your company can find to maintain your codebase. You're zero for two, my friend. :(