Pointers Are Complicated II, or: We need better language specs

[notriddle]

The discussions about formalization itself has been moved onto a separate thread, because discussing pointers in the specific and compiler IR and optimization in general in the same topic was getting to be a bit of a tangled read.

Formal specs and optimizations in general

Oh, absolutely. But when I tell the LLVM and Rust communities that the only way to solve this problem is a fully formal spec, I think the reaction would be "well that's way too much effort". OK, then lets take a quick vote. Is making a fully formal spec too much effort? @RalfJung, I think most people here know about your work with RustBelt; what do you think would need to be done to formalize LLVM IR, and then base Rust off of that formal spec? For the record, I think that while formalizi…