YHK - yet another hacker news clone

From the GitHub thread: "I think unification just generally doesn't check lifetime bounds of the type." [0]

There are steps, or rules or whatever, that perform soundness (or well-formedness or whatever) checks. And clearly one was missing.

My guess was just that maybe someone didn't think it was necessary for soundness.

[0]: https://github.com/rust-lang/rust/issues/164250#issuecomment...

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

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.

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

        $ 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;
        }

        void
        Q_free (/*@only@*/ struct Q * q)
        {
                free (q->t);
                free (q);
                return;
        }



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

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

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

                /* This is UB */
                Q_free (q);

                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:43:6: Unrecognized identifier: strdup
          Identifier used in code has not been declared. (Use -unrecog to inhibit
          warning)
        main.c:44: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:47: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:46:12: Storage l released
        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
        main.c:28:1: Function exported but not used outside main: Q_free
           main.c:33:1: Definition of Q_free

        Finished checking --- 7 code warnings

Why?

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.

Sweet. But why should anyone care..

“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.

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...

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.

Safety is a nice side-benefit. The main reason why I like the safety is because it allows you to fearlessly write high-level code without being constantly paranoid about memory as in C++. It’s more about enabling ergonomics without loosing performance, rather than security or correctness.

Consider reading past the hashtag.

But of course Python function were always duck typed so it often didn't matter to the user.

I've found type hints to be remarkably useful and catch significantly more bugs than I ever would have thought, and have quickly picked up the practice of using them wherever I code. My general finding is that if I have to struggle to put useful type hints in place, I probably need to rethink my code.

I even type hint my unit tests because I've learned that sometimes type incorrectness means my tests haven't been testing what I thought they were testing.

Frameworks like pydantic[0] can help you turn those type hints into something runtime enforcing too.

[0] https://pydantic.dev/docs/validation/latest/get-started/

The report seems to claim the opposite:

> Looking at the bug itself, it is also very likely that this unsoundness has not caused memory unsafety by accident. While it looks easy to trigger, to exploit this you need an intentionally malicious Drop implementation.

Possibly. I'm no rust expert, so I had the read the code slowly, building up a mental model of the types being used. For me, the effort that required is one of the more painful aspects of Rust.

Nonetheless when I got to this line, I stopped reading:

    q.0 = Some(&l);

I write lots of code that doesn't compile of course. It's perfectly safe because the compiler catches it. Right now, I feel like a climber at the top of a mountain who just discovered he forgot to attach his safety harness.

Who knows. Maybe all of crates.io will compile with the fixed compiler, because this is a mistake humans or LLM's never make. We will see.

Programming will never be dead.

1. Because the situation you describe is fantasy.

2. Even if it is a reality and all software can be verified (it cant), I will still be programming and so will millions of others because its fun, programming and sex are really damn close to things I cant live without. Not everyone got into engineering for the money. I legitimately love this activity, it is my actual passion. I would rather be poor than give it up.

Its like im being told everyday all day, non stop that the thing I love is not worth loving.

If your spacebar heater relies on such behaviour Rust can and will break it. If you're in the crater group you'll be notified and urged to upgrade it.

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.

I think it's a good thing to keep in mind, that the actual implementation of Rust almost certainly isn't sound. Even an "ideal Rust" still has unsafe, which can affect the soundness of even faraway safe code. But I don't think it's nessesarily wrong to talk about Rust as if it were safe. Much of our communication has implicit assumptions, and the way we talk about Rust is no different. It would be exhausting to qualify every discussion of saftey with "assuming the compiler has no bugs", "assuming all unsafe code follows the (not fully specified!) rules", etc.

Ultimately it's like any other implementation of theory into practice. The theoretical model of Rust lets us reason about and design an implementation to achieve certain practical goals even though the model is a simplification of reality. In Rust's case, practical use has demonstrated it achieves design goals like reducing bugs and reducing development time (compared to peers like C++) to a substantial degree.

Yes, you are all correct. The compiler may have a bug. And if it does not, then the type system may have a problem. And if it is formally verified, then the theorem prover might have issues. And if it does not, then the very math it relies on may be wrong.

But what do we contrast this to, what is the alternative to correctness through the type system? Almost every time, when it isn't "nothing", it's "tests". We rely on tests to test whether the program behaves correctly.

And as we all know, quite in contrast to type systems and their checkers, tests are always error-free, complete, and sensible?

Here's the current list of similar (unsoundness-causing) open compiler bugs in Rust:

https://github.com/rust-lang/rust/issues?q=state%3Aopen%20la...

Except we can't say that, at all. This is just a single bug in relatively obscure code, so 99.99999% of your code remains safe.

Meanwhile in C, 100% of your code has the potential to trigger a similar bug, except there's no path for the underlying cause to ever be fixed, unlike here.

You're essentially complaining that something isn't 100% safe, but that's just your misconception of what "safe" means. Nothing is 100% safe, not can it ever be.

It's especially ridiculous to then compare something 99.999% safe to something 0% safe and conclude that all that "supposed safety" is useless, because look: in 0.001% of cases it's NOT safe!

Considering this has gone unflagged for 11 years... Finding a flaw in Rust’s safety guarantees doesn’t mean that they provide no benefit, over a programming language without them.

Ok, but that perspective is only valid from Rust++ users who get to mog both Rust and C users. It's not a valid perspective from C users.

Also, your position against Rust is really strange to me, because I love the lack of mutable aliasing. If you think it is a punishment for the programmer you're stuck in a programming model from the 70s. Rust's model is theoretically optimal both from a hardware design perspective and a compiler perspective.

VLIW compilers love Rust because the lack of mutable aliasing by default allows aggressive instruction reordering and instruction level parallelism! Software managed caches are only possible by essentially dragging the cache coherency protocol into the software level!

The sad news is that LLVM is a classic compiler backend optimized for mutable aliasing, which means it is not that great at producing code for VLIW architectures.

Not that that would make any difference, theorem provers can also have bugs. Famously this summer someone “disproved” the collatz conjecture by exploiting a soundness bug in Lean.

no it doesn't. the broken oom behavior is distros not configuring earlyoom/systemd-oom properly. The problem here is that the kernel doesn't know what software is critical to your OS so the distro needs to be responsible for what processes to protect.

For apps that need to handle oom, Linux is missing something a handle to tell apps to shrink their memory use. Apple does this and it seems to work quite well (and proves that Linux style overcommit works well since it's what they use)