I didn't delve too deeply, but I don't get it. How do you get provable runtime safety (in a dependent types sense) in a system which gives you direct control over memory, and without introducing the kind of overhead that would be inappropriate for a systems language?
Your "overflow, then inspect" example illustrates this incoherency. If overflow is allowed, and you try to fit 250 + 10 into a u8, so the value should be 4, which is less than 10, so it should fit your precondition, not violate it. And this is a simple example where 250+10 is known at compile-time - what happens when a user provides the number at run-time? Does the compiler attempt to provide the proof anyway? How?
I mean.... I have a lot of respect for Haskell and Idris and the goals they set out. But they're not systems languages.
Your "overflow, then inspect" example illustrates this incoherency. If overflow is allowed, and you try to fit 250 + 10 into a u8, so the value should be 4, which is less than 10, so it should fit your precondition, not violate it. And this is a simple example where 250+10 is known at compile-time - what happens when a user provides the number at run-time? Does the compiler attempt to provide the proof anyway? How?
I mean.... I have a lot of respect for Haskell and Idris and the goals they set out. But they're not systems languages.