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.
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.
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.