[ktosiek]

You can use a language with dependent types (types depending on values, so you can have arrays of type "array of 10 ints" etc.) - it adds some type-level work, but makes a lot of mistakes not even compile.

But complicated type systems are, unfortunately, rarely used in languages suitable for system programming. I only know about ATS in this group actually :-)

[fusiongyro]

Dependent typing is really neat, but it introduces some new problems. Namely, the type checker becomes Turing complete. We have other examples of this level of complexity turning out to be manageable (C++ templates, for example, and the Hindley-Milner algorithm which turns out to be super-exponential in the worst case) but the power of dependent typing is begging to be used and abused to a greater degree.

I have some hope for Rust because their type invariants system (I forget what they're calling it) lets you glue some of this information to variables in a compelling way without necessarily having to solve all the theoretical and practical problems that come with full dependent typing.

We'll see, I guess.

[marshray]

C can represent the type "array of 10 ints":

     int array[10];

But probably you meant runtime variable values.

[ktosiek]

Well, here the compiler won't help you with bounded access - you can easily read array[42], and it would compile (and maybe even work... but just a little bit funny ;-)).

With dependent types function to get element from array may have type (this is pseudocode): get (array : T[n], index : m) : T {n : nat, m : nat, m < n} which would mean "function get, which takes: n long array of elements of type T, index of type m, where m is smaller than n, and returns T". Type-level naturals and bounded array access are the basic examples of dependent typing, more interesting ones may be red-black trees with guarantees about their shape put in the type or some magic for creating DSLs.

[jackpirate]

the type of that is an (int*) if I'm not mistaking

[marshray]

There's an automatic conversion to int* when necessary, but the array is nominally a distinct type. This is particularly apparent in C++ where you can do things like instantiate a template from the array type and create a compile-time function to return the number of elements.