> of debug mode always doing checked div and checked add ops. this prevents a large class of issues which you can find in debug mode. In release mode those UB checks are dropped
Checked divs are present in release mode too. Omitting them would be UB.
Other checks (e.g. for additions) are omitted in release mode, but they were not preventing UB in the first place because they guard a wrapping addition, not an unchecked one (the kind that's UB in C).
> The reason people aren’t freaking out is because most people are using heavily subsidized subscriptions.
My understanding is that enterprise plans don't offer those subscriptions, so they end up paying for API prices and models like these directly impact that revenue stream.
I think it's fairly likely medium to large corporations don't pay anywhere close to the listed API pricings as they get deals through existing partnerships with the big cloud providers.
> C is just "high level assembly" for systems programming
It is not, and that's the issue. If it was just "high level assembly" there would be no UB, and no need to have UB. Instead you have UB (although arguably not all of it is really needed) because you need optimizations, which in turn you need because otherwise C would be too slow for that "operating system" job.
> code which is called thousands of times per second
Scripting languages can easily have loops running thousand of times per second and even more. You're off by some order of magnitudes here if you want to describe operations that happen in operating systems.
I wonder how this works when a crate's type checking does indeed depend on the bodies of one of its dependency. For example `-> impl Trait` return types famously leak the `Send`/`Sync`-ness of the type, so for type checking their uses you first need to resolve the concrete type behind and hence type checking the body of the function, which seems to go against the core idea of this proposal.
I guess you could type check the bodies of only these functions, or duplicating this work in the dependencies, but this will likely have further complications especially since this will also apply to all `async fn`s.
- It would have been very annoying if it didn't work like this
- Auto-traits also leak through private fields, so you would have the same issue if you e.g. wrapped the concrete return type in a new type and returned that one instead.
Rust's AI policy does not strictly forbid AI generated code, but it does require it to be used in a kind of responsible way. What that means though it pretty abstract even to me.
As for whether this change will make it in, the devil is as always in the details and will depend on whether this solution can work for all the edge cases in the language.
So what? No one is disagreeing with you about that. The thread was about adding fine grain security controls to traditional OS filesystem access. I was just using iOS as an example, I could just have easily talked about containerization, as a security solution. Of course all those solutions are more limited than a local filesystem—the entire paradigm is designed around full control, you can't bolt on granular security. Heck, even basic UNIX permissions are pretty janky and unmanageable, but at least they more or less work everywhere since they've been around forever. Inventing something now is guaranteed to be annoying and useless.
> inspect that code and come to the conclusion that it is faithfully reproducing the exact chain of proofs we think it is
The point is that you don't need to do that. It shouldn't matter whether the proof is the one you think it is or not, only that it is a proof.
> that has literally zero bugs, however strong the type system of the language it’s writing in.
If by "bug" you mean a logic error that makes the proof invalid then Lean will catch that. Some code successfully type checking in Lean is a guarantee there are no such "bugs" (modulo bugs in Lean itself, but Lean is human written, the core is rather small, and most of it was manually proven to be sound).
Surely “the proof is the one you think it is” is the whole ballgame? Why is it impossible for a condition to be subtly reversed somewhere in the code, rendering the entire proof useless
In the real world? I’m begging for an explanation of why this is impossible because I have installed a Lean environment and it seems trivial to misname something, to mistake the order of arguments, to compare to the wrong value. There are infinitely many Lean programs that check but don’t do what they say they do, like every other language.
> Surely “the proof is the one you think it is” is the whole ballgame?
No, the important part is that the proof is proving what you think it's proving, meaning you only care about the statement being proved (i.e. the signature/type of the proof term), not the proof itself. Generally the statement will be much smaller than the proof, so manually checking it (or manually writing it) is much more viable than checking/writing the proof.
> I have installed a Lean environment and it seems trivial to misname something, to mistake the order of arguments, to compare to the wrong value. There are infinitely many Lean programs that check but don’t do what they say they do, like every other language.
Sure, that's why you have the check that the statement being proven is what you want it to be. Then any error in the proof _will_ be captured by the type checker.
Because it won't type check. It's like asking how you know some function in a program really gets an Int argument when you had lots of data structures you were passing around with all kinds of fields with various names and types.
If you construct value of type `forall n, exists m, m≥n and m prime`, then you know you have such an object. Think of a `theorem` (the Lean keyword) as a function that returns such objects. If you try to return the wrong type (e.g. you build a `forall n, exists m, m≤n and m prime`) in your "function" body, you get a compile error. If you use types incorrectly in the middle (passing values and intermediate proofs to theorems incorrectly), you get a compile error.
It's just like any programming language except the type system is rich enough that in addition to being able to have a value x: Int, (so maybe x is 5) you can have values like h: x^2≥0 (so imagine h is some object you build that proves x^2≥0).
Lemme give an example of the kind of thing I'm picturing and you can tell me where it goes wrong. Lean Web tells me the following is fine:
import Mathlib
abbrev Scalar := ℂ
abbrev Real := Scalar
theorem negative_one_has_a_real_square_root :
∃ x : Real, x * x = -1 := by
exact ⟨Complex.I, Complex.I_mul_I⟩
But we know it's a lie. I hide those abbrevs in 100k lines of stuff that you haven't yet checked manually. I don't understand what could be stopping shenanigans like these, though I appreciate you trying to show me!
I think you're misreading Lean Web. Over on the right side with that you'll see:
`Real` has already been declared
for your `abbrev Real`, and you'll see
our
Application type mismatch: The argument
Complex.I
has type
ℂ
but is expected to have type
ℝ
in the application
Exists.intro Complex.I
for the first term in your `exact` brackets.
It means that it rejects the proof. I suspect it may have been because you came back to the page too long after opening it, at which point you'll see `Lean server has stopped.` and won't get any type checking at all on Lean Web until you refresh.
But if I understand the point you're trying to make, that if you did shadow the name Real to actually mean Complex, then it would check, then yeah you're correct. But that's still where you just have to understand the statement, not the proof. The statements are never the giant 500k LoC part.
In a fixed version of your example, that means
- it's on you to understand that the statement unpacks to `∃ x : ℂ, x * x = -1`
- it's on you to look at whether the proof checker allows the proof (and potentially with what axioms, depending on your level of care)
What people are telling you is you need to check the signature of negative_one_has_a_real_square_root (which includes the definition of Real). Generally this is an easy task. Did you define things the way that you meant to define them to make the statement that you meant to make? Then you can trust that the 500k lines that prove it are fine.
If you just had what you have here in the middle of a 500k line proof of some other interesting statement whose definitions you properly validated, that would be okay. The names are weird for a human, but the mathematical content is correct.
Right but... the difference between "a robot may not injure a human being" and "a robot must injure a human being" is quite important in the real world, even if the "mathematical content is correct". And if my silly example is too contrived, it still seems like this sort of thing happens all the time:
That paper seems to just be saying that people's benchmarks are bad. Like, yeah, obviously don't consider the problem solved if the bot used sorry or axiom. This is trivial to check for and consider a compile error. It's (literally) the same as just not allowing throwing exceptions in a program. And vacuous statements aren't actually a problem. And they claim that sometimes it makes mistakes formalizing an informal statement, but that this becomes noticeable when you try to actually prove it. This is like if it forgot a parameter when it was defining a function prototype. When it actually goes to write the function, it realizes it needed some extra information, so it'll just add it. So, again, what's the problem? This isn't the type of error that can go uncaught because it won't be able to proceed with the actual proof unless it's actually true, in which case, great, it proved a stronger statement than was asked for.
A robot may not injure a human being is not a formal statement, so it doesn't even make sense to talk about here. Maybe it decides to name `Manifold` (the concept) `HumanFinalSolution`, whatever. As long as a `HumanFinalSolution` has the same formal properties as a manifold, I can still talk about the Poincaré conjecture. For formal statements, there's a compiler. Use it. It's like if I'm writing a program and I don't want it to use null, I do `-Wnull -Werror` or whatever. The task isn't done until the build is successful. I don't have to read through all the code to make sure that it didn't do null pointer dereferences or casts because the compiler doesn't allow it.
You can literally give e.g. codex a linear algebra text like Axler and a Lean setup and ask it to formalize it without using any external libraries. Do it all from scratch. I've found it'll generally be verbose, and it might e.g. use Classical.choose where it could be avoided with more work, so it doesn't prove the absolute strongest version of a theorem (which is typical for normal math exposition too), but I haven't observed it to make any of these sorts of mistakes.
After you make all your basic definitions, you can ask it to do something like solve an actual system of linear equations with a formal proof. If all of your definitions were correct, it can easily do this with a short proof from the theory. You can even give it a couple axioms from calculus, like that some functions called sine and cosine exist or whatever, along with their derivative rules, and linearity of derivatives, chain rule, etc. without actually defining what real numbers and derivatives are, and it can likewise use that to solve linear differential equations with proofs the way a high school student that memorized all of these facts would.
I actually see this as a potentially super powerful technique for teaching because you can be explicit about what did you actually prove in class versus what was a fact that I told you and maybe pictorially or otherwise hand-wavy justified, and then proceed formally from there. I think there's a lot of potential to push logic and proof assistants down to lower levels of education.
The "network" part of what they do could straightforwardly be done in a decentralized way using ordinary DNS (for the parties to discover the servers of the others) and TLS. When your card issuer is Example Bank then your "card number" would be [email protected] and the merchant or their bank knows to contact the servers at example.com to initiate a transaction for that card.
It seems like the primary thing they actually do is currency conversion, which a) isn't strictly required (e.g. plenty of small US merchants might hardly notice if they only accepted payment in US dollars), and b) could just as easily be transparently provided as an optional service by either of the card issuing bank or the merchant bank for cardholders or merchants who expect a non-trivial number of foreign currency transactions.
The real speedups in this day and age come from more efficient memory and cache usage.
reply