4 ms·
Hey, there's more than one way to overflow an integer! Trivially true things cannot depend on "fairly obvious" observations. In fact you cannot reason locally
by millstone 10y ago
Hey, there's more than one way to overflow an integer!
Trivially true things cannot depend on "fairly obvious" observations. In fact you cannot reason locally here: you must understand the whole code to convince yourself that it does not overflow. Consider an off-by-one error, like replacing line 318 with:
s=&tail[0..];
and now base will overflow.
Anyways the point of formal methods is to give yourself something better than "read carefully" to convince yourself of correctness.
- derkha 10y agoWell, that change would also break the proof in general :) . But I see your point. I've written about overflow checking some more below, but what you'd really want for that is some solid support of subtypes or refinement types - it's not just integers that have to become bounded, but also most data structures. Lean isn't quite there yet, unfortunately, but this should change in the near future with its new focus on powerful automation.