https://github.com/model-checking/verify-rust-std

hm, there's an effort but scoped only to the std

It's terrifically complex: https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/ty...

not of the implementation. Of the type system. And a verification of subsets, but not a verification of their interactions == the whole system is unverified.

That's verifying the implementation. The type system wasn't verified. It implements stuff perfectly, it has tests that prove it, but nobody formally verified that they perfectly implemented the correct algorithms

Spot on, but this makes me think of a larger problem.

You can be annoyed by Rust fanboys, sure, but the more annoying are the Rust haters, because the hate always comes from a place of ignorance.

The hate only works if you don't go beyond a surface level understanding of Rust.

E.g. a niche case on the borrow checker is slightly broken, so borrow checking doesn't make sense.

Or the "oh but Rust needs unsafe, so it's just like C++".

Yeah, but by that measure all of C++ is unsafe++, even unsafe has more guarantees than standard C++.

Only if your whole understanding of the concept is that the keyword is called "unsafe", does that argument make sense.

A bit of a rant, but if you hate Rust with a passion, ask yourself first where that opinion comes from and if it can stand on its own. In most cases it can't.

You're mistaking the semantics of the type system, from the implementation. I'm not talking about verifying the compiler. There's nothing to verify there.... literally. There is no spec to the language. By definition it is verified because the only verification you can do is tautological: "does this rust compiler do what this rust compiler does?"

But the unsoundness is because the type system itself, abstractly, was not verified. Or the interactions between parts. I.e. If you verified the compiler you'll find that it implements the algorithms perfectly. But tells you nothing about whether those implemented algorithms, however perfectly implemented, actually provided those guarantees.

Wait, there's a proven subset of C? Can you point me to some info?

While true, there are two important differences:

1) Unsoundnesses in Java's type system are checked at runtime.

2) They (or at least some) are intentional or at least won't-fix bugs.

Both are not true for Rust.

> Rust cannot fail, it can only be failed.

“Please build the perfect system. Because I specified ‘perfect’ any flaws are due to your incomplete implementation, not my awful brief.”

If the person writing the rust spec was a client I would have to drop them because they would be setting themselves up for dissatisfaction.

I don't think the definition of "memory safe" has ever required full end to end stack conformance with a proof. Very few languages have achieved that, though some have. Most people call Java memory safe, C#, Python, Typescript, etc - all of those fall short of a formally verified, sound type system with a verified toolchain.

Would you say the same thing about Java? It’s type system is also unsound.

>Rust cannot fail, it can only be failed...

Sweet. But why should anyone care..

I can't tell if you are sarcastic, but in case you are not:

By Rice's theorem you cannot be sound and complete, i.e. accept all valid programs and reject all invalid ones. Most languages choose to be sound but not complete, i.e. reject all invalid programs but also some valid ones (C and C++ are the notable exception, although most languages have escape hatches). GP was saying that the fix might reject valid programs that compile today. This is true for some existing soundness bugs, but not necessarily for this one specifically.

Also unlike C, it should be possible to formalize all of Rust, not just a subset. For two reasons: Rust evolution (not initially but today) is strongly tied with formalizing it and the language team consults with formalization experts (which are part of the Rust project themselves) all the time (and formalization or semi-formalization projects are ongoing), and also the mathematical understanding of system languages itself has advanced.

There is a severe misunderstanding here. Beside being only a subset, CompCert definitely has UB. It just formalizes codegen for codebases not containing UB, which obviously won't be enough for Rust.

Because people want a performant optimizing compiler.

Since the Rust language is defined by the Rust compiler and has no other specification, if it's UB in the compiler then it's UB in the language.

I think you are talking about a different problem and that has nothing to do with my comment.

How many of them only conditionally implement Drop, based on a generic param lifetime?

OK. That's good to know. I'm not sure why sharing our professional experience with this type of code is controversial, but here we are.

I'm not defending rust here - a correctness bug invalidates the premise. But I am saying that I've never seen a custom drop in production.

For some reason this is controversial, but it remains true.

No we're in a situation where a bug in the type checker was found and will be fixed and a new release will be made.

That it took 11 years for someone to come across this is a fairly intense counterargument to your attempt to paint this as a language with dangerous footguns.

What does "q.0" and "Some(...)" mean?

So the equivalent in C would be:

        $ cat main.c
        #include <stdlib.h>
        #include <string.h>

        struct Q {
                /*@null@*/ /*@only@*/ char * t;
        };


        /*@only@*/
        struct Q *
        Q_new (/*@only@*/ char * t)
        {
                struct Q * q = malloc (sizeof *q);
                q->t = t;
                return q;
        }

        void
        Q_set (struct Q * q, /*@only@*/ char * t)
        {
                free (q->t);
                q->t = t;
                return;
        }



        int
        main (void)
        {
                /*@only@*/ char * l;
                /*@only@*/ struct Q * q;

                l = strdup ("");
                q = Q_new (NULL);

                Q_set (q, l);
                free (l);

                return EXIT_SUCCESS;
        }

        $ splint main.c
        Splint 3.1.2 --- 21 Feb 2021

        main.c: (in function Q_new)
        main.c:15:3: Arrow access from possibly null pointer q: q->t
          A possibly null pointer is dereferenced.  Value is either the result of a
          function which may return null (in which case, code should check it is not
          null), or a global, parameter or structure field declared with the null
          qualifier. (Use -nullderef to inhibit warning)
           main.c:14:17: Storage q may become null
        main.c: (in function main)
        main.c:36:13: Null storage passed as non-null param: Q_new (NULL)
          A possibly null pointer is passed as a parameter corresponding to a formal
          parameter with no /*@null@*/ annotation.  If NULL may be used for this
          parameter, add a /*@null@*/ annotation to the function parameter declaration.
          (Use -nullpass to inhibit warning)
        main.c:39:8: Dead storage l passed as out parameter to free: l
          Memory is used after it has been released (either by passing as an only param
          or assigning to an only global). (Use -usereleased to inhibit warning)
           main.c:38:12: Storage l released
        main.c:41:22: Fresh storage q not released before return
          A memory leak has been detected. Storage allocated locally is not released
          before the last reference to it is lost. (Use -mustfreefresh to inhibit
          warning)
           main.c:36:2: Fresh storage q created
        main.c:12:1: Function exported but not used outside main: Q_new
          A declaration is exported, but not used outside this module. Declaration can
          use static qualifier. (Use -exportlocal to inhibit warning)
           main.c:17:1: Definition of Q_new
        main.c:20:1: Function exported but not used outside main: Q_set
           main.c:25:1: Definition of Q_set

        Finished checking --- 6 code warnings

The issue and none of the comments mention AI. It is pretty clear your parent said it by themselves.

I was just checking what outcome an LLM would have based on the patterns in its probabilistic distribution it has seen the wild.

Most LLMs would probably say this piece of code won't compile.