> The results of software written in languages with robust type systems. Having mathematical guarantees that your program is correct is a good place to be, but climbing the mountain to get there is, well...
It is harder, obviously, but it still tends to be a matter of understanding most of the time. But I can understand what you mean now, you are not saying it is "impossible" to do so, but that it is very hard to do so, harder than using testing (even with a lower guarantee level). If this is the case I can buy it partially, but then your point would not be as strong, I mean, we need to make a language with a good type system that can prove things reasonably well and be not that hard to use. This is more of a call to action than an impossibility question.
> See, now you're starting to understand exactly why these languages are intractable. But perhaps we can dumb things down to my mere mortal level: Why don't you use those languages for regular programming tasks?
Following my previous response: I generally don't care that much about them, because I don't find the need for them most of the time (this is part of why I said the mostly the right people matter, instead of everyone), but also because I find many of them designed in a way that is not ergonomic enough for me. This is more a design problem (that most languages have) than something else. But also, I generally use for my everyday preferred programming tasks languages that have at least powerful enough type systems, like Rust or Swift, F#, C# (because it is on the higher level of mid-tier), or even Kotlin (that I like very much, it don't has everything I like but it is closer to Swift and has a better compiler tooling) than I use languages that have not that good type-systems and resources (like Go or C), in this sense I pretty much live to my own standards, I just write tests for the things that matter and I use the type systems of those languages to prove things about my code. It works very well, and I very rarely experience problems with this, it is really satisfying for me, but I get not everyone likes this way of coding.
> How, exactly, did you reach that conclusion? You don't have to be good at something to recognize when people are bad at something.
Wdym? You don't need to be good at something, but you surely need to [understand] [better] than most people to realize those same people are worse in [understanding] and [applicability] than you.
Even knowing that you don't know something is a sign that you have a better understanding of that thing than others, but you cannot overlook to other people and say they are dumb if you consider yourself to be at the same level than them, this would be irrational to believe (because you have virtually the same knowledge and limitations).
So, if you say "most developers don't understand testing" I must get from your words, that you at least know what is a [better understanding of testing], or that you are at least more [aware] than other people about the limitations of their own testing (which implies priviledged knowledge).
But if it is the case, then an affirmation like "We'd do well to help them better understand testing" would be just pure insanity. If you believe "we" can help people understand better something, you must understand this [better] than them, there is no teacher that, ceteris paribus, know less than his students in the specific matter that he's teaching and that the student has flaws on it.
> What kind of small tests are you envisioning?
For starters, things like "is the shape of this data correct" (in the base level of any strongly typed language), and things like "was this object unitialized in the end of the scope as intended" (on the destructors feature), and things like "did I forgot to call some method, make some state change or do something else" (on the typestate concept). And even things like "is this function being possibly misused" (with type-system guarantees about mutability, nullability, aliasing and owning references, you can remove a whole class of specific tests like "is this argument invalid", "is this object being mutated outside of this function and thus being possibly in an invalid state at some point in this function", "can I be sure I can optimize this code by doing in place mutations without breaking other parts of the whole software that would be depending on it", etc). Obviously this is kind of abstract, but this is because testing is usually a pursuit of turning those generally abstract concepts onto something practical like "when the user is loging in, is the returned object in a consistent state, are the services, managers and encryption tools being properly used" or "is the customer in a valid known state at this point in the code that is significantly more complex? Can I be sure that it is not null and thus I don't need to test against it in some point?" etc.
> Furthermore, even if we grant that statement as being true for the sake of discussion, there is still the problem that the primary intent of tests is to offer documentation. That the documentation is self-validating is the reason you're not writing it in Microsoft Word instead, but that is really a secondary benefit.
First, I don't think this is true [at all]. There are many kinds of tests, and the "intent" behind them is different. For example, I can say that the primary intent of tests is to ensure the given problem and the expressed code are aligned, to check if what I did is really doing what I intended and that I did not commit any logical errors when expressing the thing, or that I was unable to express correctly what I intended to express (like if, even if everything was correct from a purely computational standpoint, I was able to effectively reach the state I was trying to consciously reach). I think a [side effect] of testing is that it turns out to be pretty good documentation for many problems, but not that it is the [intended] goal of it. Maybe if you are developing it with this goal in mind, but not as an objective unique truth.
And also, even if I accept this: type systems are extremely good ways of documenting the things you are doing. I saw many times haskell programmers say the use the types of the functions they want to call, or the things they want to make, as the way to find appropriate usages of that thing (i.e. if they need to convert a string to an int, they can search in their editor for [String -> Maybe Int] and they will find many useful functions, and probably the one they want, and everything would be very clear for them in this sense). Good types lead the programmers using them to correct code, because they make it very hard (or, sometimes, even impossible) to express incorrect programs using those types. Part of the reason I really like good type systems is that I am a very forgetful person, if I write something the chances of me forgetting about it later down the line are very high, so I really like the sensation of coming back to a codebase and finding all the clues I left for myself (i.e. the types) and discovering that for use that I need that other thing (or else it won't compile), and that function I'm calling can error in some specific signalized ways in the types (and now I remember, I need to do this and this) and how everything fits well like a good and very comfortable puzzle. This is my ideal documentation, and tests are also important for me to remember more forms of how I used this code in practicality sometimes, but many times the types are really everything I need.
This, obviously, is more anedoctal, this is how I view things, but I think many people would agree with me on this, and that this is not absurd at all as a conclusion.
--------------
I was bitten by the char limits here, so I'll put in parts
(part 1)
It is harder, obviously, but it still tends to be a matter of understanding most of the time. But I can understand what you mean now, you are not saying it is "impossible" to do so, but that it is very hard to do so, harder than using testing (even with a lower guarantee level). If this is the case I can buy it partially, but then your point would not be as strong, I mean, we need to make a language with a good type system that can prove things reasonably well and be not that hard to use. This is more of a call to action than an impossibility question.
> See, now you're starting to understand exactly why these languages are intractable. But perhaps we can dumb things down to my mere mortal level: Why don't you use those languages for regular programming tasks?
Following my previous response: I generally don't care that much about them, because I don't find the need for them most of the time (this is part of why I said the mostly the right people matter, instead of everyone), but also because I find many of them designed in a way that is not ergonomic enough for me. This is more a design problem (that most languages have) than something else. But also, I generally use for my everyday preferred programming tasks languages that have at least powerful enough type systems, like Rust or Swift, F#, C# (because it is on the higher level of mid-tier), or even Kotlin (that I like very much, it don't has everything I like but it is closer to Swift and has a better compiler tooling) than I use languages that have not that good type-systems and resources (like Go or C), in this sense I pretty much live to my own standards, I just write tests for the things that matter and I use the type systems of those languages to prove things about my code. It works very well, and I very rarely experience problems with this, it is really satisfying for me, but I get not everyone likes this way of coding.
> How, exactly, did you reach that conclusion? You don't have to be good at something to recognize when people are bad at something.
Wdym? You don't need to be good at something, but you surely need to [understand] [better] than most people to realize those same people are worse in [understanding] and [applicability] than you.
Even knowing that you don't know something is a sign that you have a better understanding of that thing than others, but you cannot overlook to other people and say they are dumb if you consider yourself to be at the same level than them, this would be irrational to believe (because you have virtually the same knowledge and limitations).
So, if you say "most developers don't understand testing" I must get from your words, that you at least know what is a [better understanding of testing], or that you are at least more [aware] than other people about the limitations of their own testing (which implies priviledged knowledge).
But if it is the case, then an affirmation like "We'd do well to help them better understand testing" would be just pure insanity. If you believe "we" can help people understand better something, you must understand this [better] than them, there is no teacher that, ceteris paribus, know less than his students in the specific matter that he's teaching and that the student has flaws on it.
> What kind of small tests are you envisioning?
For starters, things like "is the shape of this data correct" (in the base level of any strongly typed language), and things like "was this object unitialized in the end of the scope as intended" (on the destructors feature), and things like "did I forgot to call some method, make some state change or do something else" (on the typestate concept). And even things like "is this function being possibly misused" (with type-system guarantees about mutability, nullability, aliasing and owning references, you can remove a whole class of specific tests like "is this argument invalid", "is this object being mutated outside of this function and thus being possibly in an invalid state at some point in this function", "can I be sure I can optimize this code by doing in place mutations without breaking other parts of the whole software that would be depending on it", etc). Obviously this is kind of abstract, but this is because testing is usually a pursuit of turning those generally abstract concepts onto something practical like "when the user is loging in, is the returned object in a consistent state, are the services, managers and encryption tools being properly used" or "is the customer in a valid known state at this point in the code that is significantly more complex? Can I be sure that it is not null and thus I don't need to test against it in some point?" etc.
> Furthermore, even if we grant that statement as being true for the sake of discussion, there is still the problem that the primary intent of tests is to offer documentation. That the documentation is self-validating is the reason you're not writing it in Microsoft Word instead, but that is really a secondary benefit.
First, I don't think this is true [at all]. There are many kinds of tests, and the "intent" behind them is different. For example, I can say that the primary intent of tests is to ensure the given problem and the expressed code are aligned, to check if what I did is really doing what I intended and that I did not commit any logical errors when expressing the thing, or that I was unable to express correctly what I intended to express (like if, even if everything was correct from a purely computational standpoint, I was able to effectively reach the state I was trying to consciously reach). I think a [side effect] of testing is that it turns out to be pretty good documentation for many problems, but not that it is the [intended] goal of it. Maybe if you are developing it with this goal in mind, but not as an objective unique truth.
And also, even if I accept this: type systems are extremely good ways of documenting the things you are doing. I saw many times haskell programmers say the use the types of the functions they want to call, or the things they want to make, as the way to find appropriate usages of that thing (i.e. if they need to convert a string to an int, they can search in their editor for [String -> Maybe Int] and they will find many useful functions, and probably the one they want, and everything would be very clear for them in this sense). Good types lead the programmers using them to correct code, because they make it very hard (or, sometimes, even impossible) to express incorrect programs using those types. Part of the reason I really like good type systems is that I am a very forgetful person, if I write something the chances of me forgetting about it later down the line are very high, so I really like the sensation of coming back to a codebase and finding all the clues I left for myself (i.e. the types) and discovering that for use that I need that other thing (or else it won't compile), and that function I'm calling can error in some specific signalized ways in the types (and now I remember, I need to do this and this) and how everything fits well like a good and very comfortable puzzle. This is my ideal documentation, and tests are also important for me to remember more forms of how I used this code in practicality sometimes, but many times the types are really everything I need. This, obviously, is more anedoctal, this is how I view things, but I think many people would agree with me on this, and that this is not absurd at all as a conclusion.
-------------- I was bitten by the char limits here, so I'll put in parts (part 1)