native.float equality is incorrect

Stream: general

[Leonardo de Moura]

@Patrick Massot No, I was not referring to you. I will try to be super clear from now on :) I was referring to @Mario Carneiro only.

[Mario Carneiro]

I realize that I have rather extreme views on the lengths to which a programming language should strive for formal correctness. Lean 3 and lean 4 go farther than most programming languages, but not far enough for my tastes. I'm just one user though, and a programming language that tries to satisfy many users has to make compromises sometimes.

The key issue here for me is: Should we trust results proved using Lean?

There are a few ways to read that. On one hand we have pure mathematics theorems such as you will find in mathlib. Here clearly we want the kernel to be sound, and also to use axioms that are recognizable to mathematicians and true. We're doing pretty okay on that in lean 3, and lean 4 is a bit more complex but it still basically upholds this soundness property.

On the other hand we have that lean 3 has a VM, and lean 4 has a compiler, and both allow you to have code executed for things for which the logic has something to say. Here, "trusting the results proved using Lean" means that if I prove that f () = tt then if I execute it I should get tt and not ff. Here I see lots of reasons to be concerned, because we are involving a lot of external and unverified components, and while it's still "basically okay" the track record is not as clean as with logical soundness. I think this is an important property that requires vigilance to uphold.

If you are concerned so much about this problem, you should do it.

By the way, your periodic encouragements for me to do something about this are part of the reason why Metamath Zero exists, so thank you for that.

[Mario Carneiro]

I've changed the thread title to "native.float equality is incorrect" to avoid the logical consistency connotations of the word "inconsistent".

[Jason Rute]

Thanks for changing the title. :smile:

[Mario Carneiro]

We don't need an export format in Lean 4 anymore. Users can traverse all data structures and export whatever they want using the format they want.
As far as I know, Gabriel's external type checker can pretty-print the results it checked.

To clarify, you are talking about trepplein, right? This doesn't work on lean 4 AFAIK. While it's fine to say that users will write their own external typecheckers, we should have a good community story about what those typecheckers are, and how they coordinate (which necessitates a standardized export format whether or not the lean 4 core team is implementing it).

[Leonardo de Moura]

@Mario Carneiro

There are a few ways to read that.

I disagree. You gave two ways to read it. We both agree on the first interpretation.
I believe most users here care primarily about this one: logical soundness.
This is the most important property for users using systems such as Coq, Isabelle, and Lean.
The second one is about: "should we trust the code generated by Lean?"
Lean 3 is not a programming language, and I am not aware of anyone seriously using it as a programming language.

Yes, we are trying to change that in Lean 4. Lean 4 is now a programming language too.
In all public Lean 4 presentations, we clearly state that the compiler has not been verified, nor we intend to do it.
Most software developers are fine with this, and similar compromises have been done in real compilers such as ghc, clang, ocamlc, etc.
You are free to disagree, but I think this is a very good and realistic compromise.
We are making sure all mathematicians using Lean will still be able to trust the results proved using the system.
At the same time, pragmatic software developers will have a new programming language with many unique features.

I think this is an important property that requires vigilance to uphold.

This is certainly an important property, and I care about it. For sure, Sebastian and I will fix bugs in the Lean 4 compiler and interpreter.

By the way, your periodic encouragements for me to do something about this are part of the reason why Metamath Zero exists, so thank you for that.

If it is important to you, I am happy to hear you are doing it.
I do not believe this is a "pressuring issue". ITPs are still not widely used tools.
We can debate why they are not, but I am pretty sure it is not due to soundness issues.

[Leonardo de Moura]

To clarify, you are talking about trepplein, right? This doesn't work on lean 4 AFAIK.

Yes, I was referring to trepplein. My point was that even in Lean 3, users can already export their results, verify them with external type checkers, and to some extend print them using an external printer.

[Leonardo de Moura]

I do expect users will write their own type checkers and visualizers for Lean 4. In particular, if they do not trust our implementation.

[Mario Carneiro]

Lean 3 is not a programming language, and I am not aware of anyone seriously using it as a programming language.

There have been plenty of programming language-like usage of lean 3 that I have seen on this chat. The desire is certainly there, but the lean 3 VM can't quite keep up. Lean 4 is fixing this, and we're all eagerly anticipating it for this reason (among many others).

In all public Lean 4 presentations, we clearly state that the compiler has not been verified, nor we intend to do it.

The compiler doesn't need to be verified, it just needs to have no bugs in it. I think we agree that the most appropriate and pragmatic way to handle this is to wait for bug reports, treat them seriously as bugs and fix them then.

If it is important to you, I am happy to hear you are doing it.
I do not believe this is a "pressuring issue". ITPs are still not widely used tools.
We can debate why they are not, but I am pretty sure it is not due to soundness issues.

I think lean and mathlib have done a tremendous job popularizing ITPs among pure mathematicians. I don't think that soundness is actually very important towards this goal, although there are some knock-on benefits of having a stable and predictable kernel. My own work is mainly to be able to maneuver "under" the user level, to eventually be able to validate all lean (and other theorem prover) proofs with a proven-correct verifier. This work is mostly orthogonal to user level use of lean 3/4, so I'm happy to prioritize "good enough" soundness and correctness guarantees in order to prioritize ITP popularization on the lean side.

[Leonardo de Moura]

@Mario Carneiro

The compiler doesn't need to be verified, it just needs to have no bugs in it.

Yes, of course, but this is an unreasonable expectation.
The compiler is very complex, performs non-trivial optimizations, and we will keep improving and extending it.
There will be bugs, and we will fix them.
This is the compromise we keep stating in every Lean 4 talk.
That being said, I want to make it absolutely clear to everybody using Lean as a theorem prover that bugs in the Lean code generator will not affect the logical soundness of the system.
This is not the first thread written by you that generates misunderstandings and confusion about logical soundness.
To make it very clear. I am interpreting your original comments as FUD tactics (https://en.wikipedia.org/wiki/Fear,_uncertainty,_and_doubt).
I appreciate you corrected the title, and explicitly told Jason this is not a logical soundness issue.
However, you only did after I commented. Before I wrote the comment, Jason was clearly confused by your claims, figured out that there was no soundness issue by himself, and you replied with "Yes, you can argue in this way. However, ...". Really?

[Mario Carneiro]

I missed Jason's post yesterday, and responded only to today's comment. I agree with all of the things you have said, although any FUD you are reading in my words is not intentional. I will continue to clarify my statements if any additional confusion arises.