On Wednesday, 22 November 2017 at 00:49:02 UTC, Jonathan M Davis
wrote:
Any time the type system can prevent a bug, it's useful. I
don't see why that would be a problem or unwise.
That is not unwise.
What is 'unwise' is what I said was unwise..that is, putting your
trust in the compiler's capacity to always know what the truth
is. That is unwise.
Consider the Goldbach Conjecture, that every even positive
integer greater than 2 is the sum of two (not necessarily
distinct) primes. According to the principle of bivalence, this
should be either true or false.
But where is the proof that this is either true, or false?
There is a fundamental error in assuming that something can only
be either true or false. Some things require too much effort to
prove, or may simply be unprovable. How much time should the
compiler spend trying to prove something?
The question isn't whether we should use the type system to
prevent bugs. The question is which set of problems really make
sense to prevent with the type system.
No, the question should be, what can the compiler prove to be
true/false, correct/incorrect about your code, and what effort
have you made in your code to assist the compiler to make that
determination.
If you've made no effort to provide the compiler with the context
it needs to make a useful determination, then don't complain when
the compiler gets it wrong. That is my first point.
My second point, is that it is already possible to provide such
context to the compiler, without having to make reference types
non nullable, and therefore having to introduce a new nullable
reference type.
Which make more sense? Knowing that a reference type could
potentially be null, and therefore check for null, or dealing
with all the flow on conquences of making a reference type non
nullable by default?
Even with such a change, the Goldbach Conjecture still cannot be
resolved.
