Formal specs and optimizations in general

[ckaran]

@InfernoDeity

I think formalizing llvm ir, and defining rust in terms of that, is a bad thing to do. A rust implementation should not be required to rely upon llvm, so the specification itself should not be defined in terms of it.

You're right. I actually came to a similar conclusion earlier after talking with @RalfJung:

@ckaran

I guess what I'm thinking about is more along the lines of what I messaged you about privately earlier; if we had a formal IR, then we could use it as the hub of a hub and spoke of language definitions. We could define Rust (and any other language) in terms of this formal IR (FIR). Compiling would be Rust -> FIR -> LLVM IR. Proofs could be done using the FIR, but actual compilation would be done via LLVM IR. The mapping between FIR and LLVM IR would have to be constantly maintained to deal with any changes in definitions of the LLVM IR, but assuming that the FIR was designed properly, it wouldn't change.

@InfernoDeity

Rust does 100% need a formal specification of some kind, at least in my opinion. I don't think the fact that pointers are pointers changes that.

Yeah, I actually feel like the pointers question is a just a symptom of the problem. The primary cause is that without a formal definition, it's hard to do formal logic. Floating point is also a hard problem. Memory is a hard problem (different levels of caches with different accessibility, memory mapped I/O, memory mapping different address spaces together, etc.) In short, there are an endless series of hard problems, with pointers being just one small facet of the problem.