herni

I strongly disagree with the idea that Rust makes it easier to hide logic bugs. Rust is a much more complicated system than C but allows software engineers to work at a much higher level of abstraction which generally reduces logic bugs. Of course, new projects will inherently have bugs but with Rust it is easier to achieve a higher level of rigor.

To be clear, this is not due to the borrow checker at all, Rust does not have the tooling to statically determine the absence of logic bugs. What it has is the necessary programming language features to manage much more complex systems through abstraction and modeling.

This is a dumb argument imo. Critical vulnerabilities are mostly due to memory bugs (and not for a lack of other kinds of bugs). Most people relying on programs written in C (or even C++) should consider plans for migrating to software created with toolchains from this century. You cannot indefinitely carry on this tech debt.

This might sound pedantic but it is worth being precise here. These kind of issues are either "Proving the wrong statements" or "using dubious axioms". Both of these are issues not issues of the proof. You do not need to understand the proof term to identify such issues nor do you need to understand the proof term to verify their absence.

I am not saying that LEAN proofs are without issues. What I am trying to say is that the proof term itself is not the trusted part.

To be convinced of a proof, an expert will have to (1) review the definitions, (2) review the axioms, and (3) trust the kernel.

Issues can arise in all 3 but the proof itself is untrusted.

Definitions in a formal language are hard and error prone. Axioms are mostly not an issue. Most LEAN proofs should only make use of the three standard axioms (Choice, Propext, and Quotient soundness) and it is well studied what these axioms mean. Actual bugs happen in 3. Kernel bugs can for example mean that the kernel incorrectly checks a proof of "False". Kernel bugs do happen but there are measures against it (e.g., using multiple kernels to check your proof) and it is quite rare for a human to accidentally trigger one. LLMs have accidentally triggered kernel bugs in the past.

I think you misunderstand what a LEAN proof entails.

A statement corresponds to a type and to proof that statement means to show that this type is inhabitetd (i.e., there is actually a value of that type).

A proof is then "just a program" in "just a programming language". Crucially, you do not care what "this program computes" but you care only that the program actually has the given type.

There is no concept of a "bug" in a proof term because you do not actually care what a proof term "computes". You care that it exists and that it is well typed.

You miss the point here. Just because functions happen to be sets ZF does not mean sets of functions are functions. O(...) denotes a set of functions.

I disagree. Rust shines when you need perform "unsafe" operations. It forces programmers to be explicit and isolate their use of unsafe memory operations. This makes it significantly more feasible to keep track of invariants.

It is completely besides the point that you can also write "shit code" in Rust. Just because you are fed up with the "reimplement the world in Rust" culture does not mean that the tool itself is bad.

Gotta love the classic "everyone else is cheating too"

MrBeast is not just a YouTube channel but a huge business/brand and should be held accountable at much higher standards.