A language meant to replace C should offer more correctness guarantees, and sometimes people have found ways to do it that surprise me. This paper shows a (quite cute) type system that works on spans of bits of integral numbers, that I think is able to catch some of the bugs of the kind of low-level code you see in C/C++/Rust/Ada:
http://goto.ucsd.edu/~rjhala/papers/bit_level_types_for_high_level_reasoning.html
The paper first of all proposes a type system to manage bit ranges and bit operations in a safer way. The paper use this short code example:
mget(u32 p) {
if (p & 0x1 == 0) {
error("permission");
}
pte = (p & 0xFFFFF000) >> 12;
b = tab[pte] & 0xFFFFFFFC;
o = p & 0xFFC;
return m[(b + o) >> 2];
}
To represent the type of those variables they use sequences of {name,size} pairs (a semicolon means field with no name, often filled with zeros), like:
p: {idx,20}{addr,10}{wr,1}{rd,1}
pte: {;,12}{idx,20}
b: {addr,30}{;,2}
o: {;,20}{addr,10}{;,2}
Once you have given a name to those bit spans you can think of using a field access syntax:
mget (p) {
if (p.rd == 0) {
error("permission");
}
pte.idx = p.idx;
b.addr = tab[pte.idx].addr;
o.addr = p.addr;
return m[b.addr + o.addr];
}
Their paper also uses some type inference, so you don't need to specify the spans manually. An example of the output of the type inferencer:
typedef u32 BOT_t;
typedef u32 k_t; typedef u32 s_t;
typedef u32 b_t; typedef u32 r_t;
struct __b0 { k_t k_1; BOT_t BOT_2; };
struct __b1 { BOT_t BOT_1; k_t k_2; };
struct __b2 { b_t b_1; r_t r_2; };
struct __b3 { b_t b_1; BOT_t BOT_2; };
struct __b4 { BOT_t BOT_1; b_t b_2; BOT_t BOT_3; };
struct __b5 { k_t k_1; b_t b_2; s_t s_3; };
u32 mget(struct __b5 p ) {
struct __b0 p1; struct __b1 pte;
struct __b2 b1, tab[1000];
struct __b3 base, a; struct __b4 off;
if (p.s_3 == 0) {
error("Permission failure");
} else {
p1.k_1 = p.k_1; p1.BOT_2 = 0;
pte.BOT_1 = 0; pte.k_2 = p1.k_1;
b1.b_1 = tab[__b1_to_u32(pte)].b_1;
b1.r_2 = tab[__b1_to_u32(pte)].r_2;
base.b_1 = b1.b_1; base.BOT_2 = 0;
off.BOT_1 = 0; off.b_2 = p.b_2; off.BOT_3 = 0;
a.BOT_2 = 0; a.b_1 = base.b_1 + off.b_2;
return m[__b3_to_u32(a)];
}
}
From the paper:
The type inference algorithm constructs bitvector types for the variables and the translate procedure constructs C structures corresponding to these types, where each field is an unsigned 32 bit entry. The field BOT_n refers to a zero block in the type. For example, the structure struct b5 encodes the bitvector type {k,20}{b,11}{s,1} and struct b1 encodes the type {;12}{k,20}. The assignments are translated to structure assignments. For array indices, we convert the bitvector structure to the corresponding integer by a system-defined function (to allow array indexing by the structures).
So they use unannotated or lightly annotated C code, run the bit type inferencer on it, and verify it's "correct".
I guess you can implement the same type system with a rustc plug-in, and use it for regular Rust code. Later that plug-in could become part of rustc. But are the safety advantages of this unusual kind of type system worth the implementation efforts?
(Writing rustc plugins that add relatively simple type system extensions (like some of the features from Ada language) is something I'd eventually like to do).