[Cladode]

   partially initialized arrays

I agree that partially initialized data structures are important for low-level, performance-oriented programming. But it is not clear how to do this within a Rust-style type-based approach to memory safety. Naturally, one can always wrap the problematic code that deals with partially initialised data in an unsafe-block, but you can already do that in Rust. By Rice's theorem we know that we cannot have a feasible typing system that allows us always to deal with partially initialised data in a safe way, but could there be a compromise, covering most of the standard uses of partially initialised data (e.g. what you find in a standard algorithm text book like CLRS, or a standard library like C++'s)? I don't see how right now, because the order of initialisation can be quite complex, too complex to fit neatly into well-bracked lifetimes a la Rust.

Have you got any ideas how to do better?

[Animats]

Sure, having dealt with this formally in 1981 with machine proofs.[1]

In the Pascal-F verifier, we treated array cells as if they had a "defined()" predicate. Clearly, if you have a flag indicating whether an array cell was defined, you could handle partially initialized arrays.

Then you prove that such a flag is unnecessary.

We had a predicate

    DEFINED(a,i,j)

which means the entries of the array a from i to j are initialized. Theorems about DEFINED are:

    j<i => DEFINED(a,i,j) // empty case is defined 

    DEFINED(a,i,j) AND DEFINED(a,j+1,k) => DEFINED(a,i,k) // extension

    DEFINED(a[i]) => DEFINED(a,i,i) // single element defined
 
    DEFINED(a,i,j) AND k >= i AND k <= j => DEFINED(a[k]) // elt is defined

Given this, you can do inductive proofs of definedness as you use more slots in an array that started out un-initialized.

To do proofs like this, you have to be able to express how much of the array is defined from variables in the program. Then you have to prove that for each change, the "defined" property is preserved. Not that hard when you're just growing an array. You can construct data structures where this is hard, such as some kinds of hash tables, but if you can't prove them safe, they probably have a bug.

This was new 40 years ago, but many others have been down this road since. Rice's theorem isn't a problem. That just says that you can construct some undecidable programs, not that all programs are undecidable. If your program is undecidable or the computation required to decide it is enormous, it's broken. Microsoft puts a time limit on their static driver verifier - if they can't prove safety after some number of minutes, your driver needs revision. Really, if you're writing kernel code and you're anywhere near undecidability, you're doing it wrong.

[1] http://www.animats.com/papers/verifier/verifiermanual.pdf

[Cladode]

Thanks.

We were talking cross-purposes. I was thinking about partially initialized arrays in the context of a Rust-like type-checker. I don't think the analysis you ran in 1981 in a prover is possible in 2020 in a type-checker, at least without putting most of the bits dealing with partial initialization into unsafe-boxes.

It would be great if Rust-style type-based lifetime analysis could cope with partial initialization.