Lean ABI stability

Stream: lean4

[Mario Carneiro]

While looking at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lazy.20lists/near/271108904 , it occurred to me that there are various functions in lean core and elsewhere that deliberately do "type punning" of lean objects, and I'm wondering how reliable we should consider this kind of code. In the example, we are relying on the fact that the encoding of inductive types (with more than one constructor) as a numeric tag plus fields means that adding more constructors at the end of the list is not ABI breaking. NonScalar is also used for type erasure in the core library.

• Does the compiler / runtime make any promises about validity of casts? For example, is casting Type to Unit safe?
• Can we cause C undefined behavior by abusing unsafeCast? (My guess: yes)
• Do we expect users (incl. library developers) to be able to use unsafeCast safely and stably?

My impression is that unsafeCast is supposed to be an official part of the language, and we are not planning on declaring all nontrivial casts as UB, meaning that we should probably document somewhere what the ABI is and the impact of this for reviews of use of unsafeCast.

Of course there isn't really anything in lean that is "stable" right now, but ABI stability seems more problematic than other areas since most lean changes cause compile errors, while this one can (potentially) introduce UB in a working project. A static checker for simple cases of unsafeCast might even be possible to help control this.

[Sebastian Ullrich]

Some recent discussion on validity of casts: https://github.com/leanprover/lean4/pull/956

[Sebastian Ullrich]

The current situation isn't too different from Rust's for the longest time - it took them years to figure out when an unsafe block can actually be considered safe. I don't know the exact state of GHC's unsafe ops, but I wouldn't be surprised if their guarantees are mostly informal as well.

[Sebastian Ullrich]

The first answer as to how to use unsafe* should of course be: don't

[Leonardo de Moura]

After the Mathlib port is complete and all missing tactics are implemented, we are planning to work on the compiler again. We expect this will happen at the end of 2022 or the beginning of 2023. We want to move all the remaining C++/C compiler code to Lean, but we also want to implement missing features and have better support for debugging information. Some of the planned new features will break ABI. For example, we want to add support for stack-allocated objects. This is useful, for example, when a function returns a pair.