It's always amazing to me that abstractions are so fragile in practice we still haven't managed to fully abstract over numbers.https://twitter.com/JonMLevine/status/1044950721857298432 …
This is equivalent. Just add if (x>K) return error; (or assert) before the arithmetic. No need to put runtime check in the language's def of arithmetic.
-
-
It's sometimes non-trivial to propagate "no overflow" back to a bound on the inputs. Letting compiler insert `jo` for you is a useful model.
-
Better still when the compiler can insert it *only* where it can't prove that it's unnecessary, and give you that feedback.
-
In some cases it would generate slightly more optimal code, but it makes the language more complex and hard to use, I think.
-
Depends. If your goal is "make this as efficient as you can, but more importantly make it correct", it's a pretty nice solution. If your goal is "I want extremely precise manual control over the instructions generated", then yeah, it's probably not what you want.
-
The former seems like a correct characterization but the latter seems off-base. My intent is to require write-/compile-time intervention in the form of some condition that feeds into a proof of boundedness when a proof does not emerge in an automatable way.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.