IEEE 754 Float

Stream: lean4

[Alex Sweeney]

I assume the basic Float type is the binary64 format but Float.lean doesn't tell me much about what exactly it is or how it works. Are IEEE 754 floats and float arithmetic implemented in pure Lean somewhere?

Disclaimer: I'm still new to Lean. I did try to find the docs but the page for Float is blank (https://lean-lang.org/lean4/doc/float.html)

[Mario Carneiro]

Float is an opaque type from lean's perspective, but yes it is in fact IEEE 754 binary64

[Alex Sweeney]

@Mario Carneiro As far as I can tell opaque is a way to define something that's unknown to the type checker. Is this so it can use C's float math for performance reasons? Or they just didn't want to reinvent floats in Lean? Basically I think it would be neat to prove things about IEEE 754 floats and I'm a little confused why it seems nobody has done it. Sounds like a fun project.

[Andrew Yang]

Might be relavent: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/IEEE.20floats

[Henrik Böving]

Yes it is for performance reasons. The compiler knows about Float as a primitive type and turns them into the proper C type. I guess if you really want to you could redefine them as UInt64 and start formalizing things about them but at the time that the current float implementation was conceived there was basically no use for theorems on it so nobody did it.

[Utensil Song]

Personally, I would be interested in formalizing (or seeing the formailzation of) something like Herbie which is about "Automatically Improving Accuracy for Floating Point Expressions", see also here for a series of rewrite rules, they are supposed to be equal for $\mathbb{R}$ and reach a better accuracy bound for floats. I hope to formalize not just IEEE 754 float but also emerging float types like bfloat16 or 4-bit NormalFloat which is supposed to be an information theoretically optimal type for quantization in the area of LLM research.