Shawn Garbett wrote:
I dislike the + operators with source and result values being different types because the result can not be reassigned to a source variable. This makes using + to increment variables difficult, or at least unintuitive.
I didn't make myself clear. On a side note, I'm still
fiddling with getting the environment compiled and
absorbing the language documentation.
It was my understanding that BitC was static typed. So if + is allowed to have the following types:
+ :: int8 -> int8 -> int16 + :: int16 -> int16 -> int32 + :: int32 -> int32 -> int64 + not defined for int64.
One would be free to use a straight + or -, as long
the target variable is of the correct size to handle
the result.
As I recall, the original discussion is assumeimg that programmers often forget the condition where + overflows, and we are trying to help them catch this error. If so, I think an interesting question to ask is: "Which of bounded+ and wrap+ is a check on the overflow condition more likely to be included by proofs the programmer writes?"
I believe a novice programmer is very likely to attempt proofs directly involving exceptions, and proofs indirectly requireing that many possible exceptions are not thrown. I think the first proof most programmers will think of is: "my program throws no exceptions." However, I have no data to support that these proofs will be more common than those requireing that overflows have not occurred.
Scott Doerrie
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
