| > Tests don’t catch everything. Again, they will catch your runtime errors if your behaviour is covered. If your behaviour isn't covered, then you're just shifting the problem to the program doing the wrong thing instead of crashing. That is not a win. It might even be worse! So, this doesn't matter in practice. Your purely academic view of the world doesn't work with the discussion taking place, I'm afraid. > If you had a language that probably does not have runtime errors you don’t even need one test. Go on. Here, let's use your example: > That’s (p2 - p1 / t2 - t1). Traditionally, the calculation is (p2 - p1) / (t2 - t1). I'll assume you had a non-standard situation that necessitated a different formula, but this could have equally been a mistake. It wouldn't be too hard to forget the inner parentheses. We'll assume that divide by zero was already eliminated by the type system, but now show us how sum types would avoid someone from making that mistake. Maybe you did need tests after all... > You’re writing this because you don’t have experience with programs that can never crash. Not so. I spend most of my days writing code in programming languages that do provide such guarantees. It is a cool party trick, but doesn't really matter at the end of the day because they still don't offer the expressiveness to ensure that the program does what is expected of it. I still have to write tests, and once I've written the necessary tests to ensure all the behaviour is correct, there is no practical way you can miss a crash situation. > Our integration tests and unit tests have dozens of tests that never yielded an error and we never saw an error in production for years. And had you avoided the crash you'd get erroneous results from the function instead. You're not really any farther ahead. You still need assurances that the function actually behaves correctly. And if you had those assurances, you'd have caught the divide by zero condition. You're not going to convince me that a complete type system is academically better. I already agree with that. But absent a complete type system, you're going to have to resort to tests. Once you've written those tests, you're going to uncover the runtime errors anyway. > Division by zero. We had a crash in production. Your fuzz tests never tried passing in values that would lead to division by zero? For such a simple function that has many possible states that can lead to that condition, that seems completely inconceivable. Hell, I just tried it for fun and it found the issue in less than 100 tries! This must have been the time you were talking about where you deployed to production without running the tests? But let me be try to be clear: The compiler warning you that you haven't considered a division by zero case does not mean you've handled it correctly. Absent a complete type system, you still need tests to ensure that the behaviour is consistent with expectations even in those edge cases. But with those tests, runtime errors can't go unnoticed anyway, so you didn't really need the type system. > Better to prove the function works via proof Agreed. Complete type systems are unquestionably better theoretically. Writing tests is tedious. But it remains that with the languages people actually use, even those with "advanced" type systems, you can't prove much. You have to fall back to testing, and at that point you're going to uncover the runtime errors too. > You’re inexperienced that’s why you’re fascinated. There's a good way to change that. Let's see your code! |
So you're saying write tests that cover every possible behavior. Makes sense right? It's like saying write code without any bugs. Simple! You're not getting it. You can go run around telling people to write tests that eliminates 100% of bugs and that if you think that will eliminate all bugs from the world, well you're just not experienced.
>Go on. To continue with the original example, I have a function that tries to write to a file. If that fails, the caller is to try to write to a file on a different device. If the caller does anything else the program is broken with serious consequences and should not be shipped to production. Express that expectation using sum types. Hell, express it using any type construct available in popular languages. Good luck!
You can do this on rust. Literally it's the core of the rust sum type system. Good luck? Have you done basic programming with rust? Here's some psuedo code:
The above is psuedo code. The thing with the match operator is that the program DOES not compile if you do not handle both SOME and ERROR. For golang you can handle the Some and then it crashes if there's a problem. You aren't required to explicitly handle it.>Not so. I spend most of my days writing code in programming languages that do provide such guarantees. It is a cool party trick, but doesn't really matter at the end of the day because they still don't offer the expressiveness to ensure that the program does what is expected of it. I still have to write tests, and once I've written the necessary tests to ensure all the behaviour is correct, there is no way you can miss a crash situation.
There is a way. You're just not getting it. there's about infinite ways to crash a program that has runtime errors.
>Your fuzz tests never tried passing in values that would lead to division by zero? For such a simple function that has many possible states that can lead to that condition, that seems inconceivable. Hell, I just tried it for fun and it found the issue in less than 100 tries! This must have been the time you were talking about where you deployed to production without running the tests?
Hell I used a programming language with no run time errors and I didn't write a single test. Amazing! There are tons of functions complex enough such that your fuzz test will miss it. Again we had this code working for years because we implictly assumed said devices will never pass duplicate data.
Also we don't write fuzz tests. We just do basic testing. Fuzz testing is something our start up doesn't have time for. We would prefer guarantees without the need of extra testing/work/time in this area.
>Traditionally, the calculation is (p2 - p1) / (t2 - t1). I'll assume you had a non-standard situation that necessitated a different formula, but does serve as a great example of how behaviour is your real concern. One could easily input the formula you gave where they expected (p2 - p1) / (t2 - t1) and sum types wouldn't care one bit.
Nope your formula is correct. I just assumed you were intelligent enough to know what I meant even though I didn't put in all the parenthesis (I'm typing on my phone afte rall). I thought wrong.
>Agreed. Complete type systems are cool. Writing tests is tedious. But we await your proof to my case for a realistic setting where one uses a typical production programming language. If all you have is silly half-measures that only cover a small number of cases, you're not really proving much. All you are doing is giving yourself a false sense of security.
Yes rust. Jesus. You're so inexperienced you don't even know when it's standing in front of your face. You don't need the borrow checker from rust. You only need the sum type. Then take the sum type apply it to division by zero and out of bounds array access and all IO calls. Boom that's it. No more runtime errors.
>There's a good way to change that. Let's see your code!
just look at elm man. Yuo don't even know what I'm talking about because you literally don't have experience. You want to see code that never crashes? Get some experience with Elm and you'll see why it never crashes and you'll see it doesn't take a "complete" type system to make it that way. Elms type system is woefully simplistic.
Rust is like 80% of the way there... the reason why people don't use it is lifetimes and the borrow checker and the complexity associated with it. Additionally rust left some holes so it can crash (like division by zero), but it has all the primitives needed to prevent it.