[jstimpfle]

> by encoding my invariants in the type system

the way I program that is nothing but a pipe dream.

> If you "know" that the value is present rather than absent, you must have a reason for knowing it, so explain that reason to the compiler.

I might know that it exists for example because it is computed in a post-processing step after a first stage but before a second stage. So it exists in the second stage but not in the first. Relying on global data (which I won't give up) makes it practically impossible to encode that the data is not there in the first stage.

And that's not a problem at all. I simply don't access that data table in the first stage... Trying to explain my processing strategy to a compiler would amount to headaches and no benefits.

[lmm]

> I might know that it exists for example because it is computed in a post-processing step after a first stage but before a second stage. So it exists in the second stage but not in the first.

So the first stage could create a handle to it, or even just a phantom "witness" that you treat as proof that the value is present.

> And that's not a problem at all. I simply don't access that data table in the first stage... Trying to explain my processing strategy to a compiler would amount to headaches and no benefits.

Shrug. I found that errors would make it into production, because human vigilance is always fallible. And the level of testing that I needed to adopt to catch errors was a lot more effort than using a type system.

[jstimpfle]

Accesses to unallocated global data is the type of errors that you typically hit on the first test run. Another example would be function pointers loaded from DLLs.

I don't think type systems help all that much. Type + instead of -, and you're out of luck.

[lmm]

> Accesses to unallocated global data is the type of errors that you typically hit on the first test run.

Depends what conditions cause it; the hard part is being sure that every possible code path through the first stage will initialise the data, even the rare ones like cases where some things time out but not others.

> I don't think type systems help all that much. Type + instead of -, and you're out of luck.

Not my experience at all - what do you mean? If you declare a type as covariant instead of contravariant or vice versa, you'll almost certainly get errors when you come to use it.

[jstimpfle]

1) Pretty easy to guarantee if main looks like stage1(); stage2(); stage3(); etc.

2) Change a plus for a minus and it is still an int.

[lmm]

> 1) Pretty easy to guarantee if main looks like stage1(); stage2(); stage3(); etc.

You can only use the global program order once, I'd rather save it to spend on something more important. val result1 = stage1(); val result2 = stage2(result1); ... means my code dependencies reflect my data dependencies and I'll never get confused about what needs what or comes before or after what (or the compiler will catch me if I do), so I can refactor fearlessly.

> 2) Change a plus for a minus and it is still an int.

True. If you get your core business logic wrong then types won't help you with that (though FWIW I'd argue that it's worth having a distinct type for natural numbers, in which case - and + return different types). But I found that at least 80% of production bugs weren't errors in core business logic but rather "silly little things": nulls, uncaught exceptions, transposed fields... and types catch those more cheaply cheaper than any alternative I've seen.