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 …
-
-
In any case, a runtime check is only meaningful with runtime sizing, meaning your language model has allocation going on under the hood, which means it's not suitable for low level programming of any sort.
-
No, a runtime check is useful even without runtime sizing. I may have a computation on i64s that I believe cannot overflow, but I can't prove it to Z3's satisfaction--I'm offering a pragmatic option of "I don't think this will ever happen, but if it does, error out of the \
-
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.