WUFFS types can be refined as well as having a native representation so e.g.
base.u8[0 .. =99] is a single byte with values from 0 to 99 inclusive
base.u16[0 .. =99] is a 16-bit type with the same values
base.u16[100 .. =400] is still 16 bits but values from 100 to 400 inclusive
In WUFFS all arithmetic overflow or array bounds misses are compile time errors. From the point of view of WUFFS if pixels is an array with 200 elements, and idx is a base.u8[0.. = 240] then pixels[idx] is a type error as it wouldn't make sense to index 240 into an array of 200 elements so that doesn't compile.
As well as the obvious safety implication, this also means WUFFS can in principle go just as fast as if you were inhumanly careful with a conventional low level language and skipped any safety checks, since it knows it already took care of that. In practice it transpiles to C (which doesn't know what safety checks are).
base.u8[0 .. =99] is a single byte with values from 0 to 99 inclusive
base.u16[0 .. =99] is a 16-bit type with the same values
base.u16[100 .. =400] is still 16 bits but values from 100 to 400 inclusive
In WUFFS all arithmetic overflow or array bounds misses are compile time errors. From the point of view of WUFFS if pixels is an array with 200 elements, and idx is a base.u8[0.. = 240] then pixels[idx] is a type error as it wouldn't make sense to index 240 into an array of 200 elements so that doesn't compile.
As well as the obvious safety implication, this also means WUFFS can in principle go just as fast as if you were inhumanly careful with a conventional low level language and skipped any safety checks, since it knows it already took care of that. In practice it transpiles to C (which doesn't know what safety checks are).