Comment by Animats
7 years ago
That’s a dream for the far future.
Which it has been for too long. I was doing automated program proving on basic validity stuff like this over 30 years ago.
In order to prove something, you first need a notation for talking about it. Few languages let you talk about uninitialized memory space properly. Constructors are too magic.
Un-initialized memory can be viewed as write-only. You want to show that no un-initialized byte is ever read. Memory comes from the allocator in blocks of un-initialized bytes.
A constructor is simply a function that takes a block of un-initialized memory and assigns every byte to something meaningful for that type. At the end of construction, the memory block becomes a valid instance of that type.
Once you can talk about construction as a non-magic operation, you can talk about partial construction of an array. Until you can talk about it, you can't prove anything about it.
Some types, such as "byte", are fully mapped - any bit pattern is valid. So they can be initialized by anything that fills them. That's how input buffers can be expressed.
Note that Rust essentially expresses all of that. It has no magic constructors, and Vec is a block of uninitialized memory along with safe partial construction of array.
It's true that it's dynamic construction (although other similar constructs allow for doing it for statically sized arrays), but it is demonstrating Rust's power: making safe APIs over `unsafe` code without having to delve into the depths of a complicated compiler/proof-assistant. This is exactly what `unsafe` is for: extending what safe code can do by temporarily stepping outside the bounds of what the language directly encodes.
> A constructor is simply a function that takes a block of un-initialized memory and assigns every byte
In C++, the constructor doesn't initialise every bytes (padding for example)..
Then you need to show that any un-initialized byte can either never be read or is of a fully mapped type where it doesn't matter.
I'm not sure what you mean by 'a fully mapped type' but uninitialised padding bytes are read without problem in C++ when you do a memcpy of a structure..