[bitc-dev] A Modest Proposal (was: Primary type arithmetic)
Jonathan S. Shapiro
shap at eros-os.org
Mon Feb 7 11:36:32 EST 2005
So far as I can tell, I am making only one of the assumptions that you
have enumerated. I cannot speak for anyone else in the group.
> * BitC programs will in general be fully specified, so if a program's
> correctness depends on a + operator, of whatever form, to not overflow, this
> dependence will be captured by way of proving the program satisfies its
> My take: Most BitC programs, like most regular programs, will only be fully
> "specified" by their source text....
> BitC will move programming towards being a more formal activity, but it will
> remain a mostly informal human activity, and the source notation must continue
> to be a good user-interface to this activity.
I certainly do not make this assumption, but if we actually accomplish
your last sentence, that would be wonderful.
> * We will generally try to prove that programs are both safe (consistency is
> preserved) and live (forward progress continues).
This seems vanishingly unlikely, except for the small number of critical
programs that you allude to.
> * There are times when a C programmer says "+" where it might wrap, and where
> the program will still be correct if it does.
The discussion on this topic remains open. Rather than ascribe opinions,
perhaps it would be more appropriate to simply state what *you* believe.
I think that the characterization you give below is about right:
> When a C programmer says
> "+", they either have reasons to believe that it won't wrap, or they don't
> care if their program is buggy if in those cases.
This (your statement above) is the actual assumption that I privately
would bet on, but as I say above, the issue remains open.
> * On Pentium architectures, in the absence of proof that we're safe from
> overflow, the overflow check can only be done by an explicit check, which is a
> cost that will deter C programmers from switching to BitC.
> My take: These same C programmers will be deterred by the bounds check on
> array indexing...
This is an assumption that I am actually making. The difficulty with
your rebuttal is that my "assumption" is amply supported by empirical
evidence. Given which, I am reluctant to take a final position on the
behavior of integer operators until I understand the difficulty of
discharging the "does not overflow" lemma.
More information about the bitc-dev