Dependent types allow for this kind of thing.<p>Another possibility that doesn&#x27;t require such heavy language machinery is something like OCaml&#x27;s private types, where the scope of unrestricted access is unsafe blocks rather than the body of a module. In this approach there is no type-level correspondence between the value of the length member and the extent of the array: private types only ensure that any potentially invariant-breaking mutation is restricted to a certain scope, not that the code is correct.