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 _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
