There are varying degrees of "proof", ie. we can have more or less
confidence in an argument. In particular, we need to distinguish between "Mathematical proof" and "formal proof".
Mathematical proof is what we tend to think of when we see the word "proof", and it can be defined something like "a thoroughly convincing argument".
A "formal proof" is very different. If we're given a finite set of strings, and a finite set of string-rewriting-rules, then a "formal proof of X" is just "the order in which to apply the rules, such that we turn the given strings into X".
For example, the rule called "modus ponens" says:
If I have strings of the form "X" and "X -> Y", then I can get the string "Y"
If I'm given the modus ponens rule, and the strings "A", "B" and "A -> B -> C", then this is a proof of "C":
1) A -> B -> C (given)
2) A (given)
3) B -> C (modus ponens with 2 and 1)
4) B (given)
5) C (modus ponens with 4 and 3)
When formal proofs were introduced, the idea was to choose the given strings (axioms) and rules such that "formal proof" meant pretty much the same as "Mathematical proof", ie. that formal proofs are convincing and that non-formal proofs aren't.
It's pretty easy to see that type systems (including Java's) are formal systems. The "given strings" are the types with primitive values, ie. I am 'given' the string "bool" since I can always say "true" or "false". The Java equivalents of strings like "A -> B" are methods, with argument type "A" and return type "B". The modus ponens rule says "calling a method with an argument of the correct type gives the result type" (ie. "A -> B" and "A" gives "B"). The Java equivalent of formal proofs are Java programs.
From this perspective, type-checking a Java program is checking the formal proof it represents; ie. ensuring that we only use the rules we were given (anything else is a syntax error, like `bool(5)`) and that the strings match up (eg. that we don't use modus ponens on "A" and "B -> C", which is a type error, like `3 + "hello"`).
> Academics tend to think it is a big deal because it makes it harder to prove programs correct, but almost nobody does that with Java programs, so it doesn't really matter to most programmers.
In fact, it's the exact opposite: every time a Java programmer compiles their code, they are formally verifying that their program is correct. The only Java programmers who don't prove their programs are correct are those few who've never compiled their code.
That might seem pedantic, ie. that I've redefined "proof" to win an argument, but in fact that alternative definition has been around for a century and, more importantly, it is the one PL researchers use (I should know, I am one ;) ).
The reason academics don't like NULL isn't that it makes proving things harder; it's that it makes proving things too easy! Java types are formal statements, by definition; Java programs are proofs of those statements, by definition; we have a whole bunch of machinery for checking these types, IDEs with auto-completion, automated refactoring, etc. so why not use it to prove stuff we care about? For example, a crypto library could encode some security properties as types to make sure consumer classes are using them properly. Then we could have our application require proof that our implementations are correct, like this:
// Works for any LoginComponent, as long as it uses crypto in a provably safe way
final class Application<LoginComponent> {
public Application(LoginComponent lc, UsesCryptoSafely<LoginComponent> proof);
// ...
}
The reason Java programmers don't do this
isn't that it's too hard. It's that it's far too easy:
Application<MyLogin> app = new Application(new MyLogin(), NULL);
So easy, in fact, that it's
useless: we can use "NULL" to literally prove
anything in Java. These are still "formal proofs", but they're very far away from "Mathematical proofs", ie. telling me that your Java program type-checks doesn't convince me that it works the way you want, precisely because the axioms and rules used in Java cannot be used to convince me.
This isn't an ivory tower, pedantic, academical issue; it's an incredibly practical piece of software engineering: we want to find as many bugs as possible for the smallest cost possible. Java is already paying a high cost for its type system, especially since it has no type inference. Yet the existence of NULL undermines it's usefulness for spotting bugs. Basically, Java hits an "anti-sweet spot" where we must annotate everything explicitly and architect our programs to work within the type system's constraints, yet it doesn't give us much confidence that we've squashed bugs.
Compare this to un(i)typed languages like Python, where we don't need annotations and our architectures aren't as constrained; we lose a little confidence but we save a huge cost.
Compare this to strongly typed languages like Haskell, where we're constrained by the type system and we occasionally need a couple of annotations, but we gain a large amount of confidence for that price.
> the language needs a way to represent the state that an object starts out with. For integers and floats that is 0, for booleans it is false, and for objects it is null.
I think you're confusing values with variables. The only value (object, etc.) which is NULL is, well, NULL. You can't change a NULL into an initialised instance; you can only replace it.
You can initialise a variable to be NULL, then redefine it to point at an object later. In that case, I'd say you should either be using an Optional value, or you're initialising your variable too early.