[tialaramex]

> explicit focus on correctness, simplicity and verification

Does this mean Cranelift has a clearer view of what its IR really means than, say, LLVM? It seems to me that being very clear-eyed on this will be important as C and C++ get ready to bite the bullet (perhaps this decade) and formally document how pointer provenance works in their languages, and perhaps Aria's provenance "experiment" in Rust begins the journey to stabilisation.

[cfallin]

That's the goal at least! We explicitly do not have a notion of "undef" or "poison" values in our IR, and to the largest degree possible we want determinism (modulo e.g. some NaN-related stuff right now). Our current discussion with some researchers wanting to formally verify our lowerings will likely push us toward the start of some formal spec for the IR as well, though exactly how that will work or be maintained is not yet decided.

I'm not super-familiar with the pointer provenance work in Rust but I'll read more about this; thanks for the mention!