[bitc-dev] A Modest Proposal (was: Primary type arithmetic)

[Jonathan S. Shapiro]

Mark:

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 
> specification.
> 
> 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.

shap