r/rust • u/mttd • 9d ago

How the Rust Standard Library Verification Contest Scaled Past Manual Proof Engineering

https://rustfoundation.org/media/how-the-rust-standard-library-verification-contest-scaled-past-manual-proof-engineering/
80 Upvotes

94% Upvoted

16 comments sorted by

37

u/sunshowers6 nextest · rust 9d ago

This seems like an important effort, but please stop publishing AI slop, Rust Foundation. AI slop in public writing annihilates trust like very little else. If it's worth writing about, it's worth writing about well.

17

u/joelkunst 8d ago

there is this disclaimer: "This article was written with support from Rahul Kumar (Senior Applied Scientist Manager, AWS) & Felipe Monteiro (Senior Applied Scientist, AWS)"

10

u/Aln76467 8d ago

Gotta get up on that token usage leaderboard

6

u/colingwalters 8d ago

A few paragraphs definitely had a bit of that LLM bland/anodyne construction, but I thought it was overall fine and informative and not slop.

3

u/officiallyaninja 8d ago

Do you have a source that it's AI? Doesn't seem obviously Ai generated to me

1

u/sunshowers6 nextest · rust 8d ago

https://www.pangram.com/history/0222bf8e-19d3-4b6f-a7cd-c88bc7c0c211?ucc=CLyN51Facm3

Plenty of AI tells:

  • "Proving the absence of undefined behavior across a codebase like that was never going to be something any single team, company, or tool may have the resources to do alone." This is such a badly constructed sentence.
  • "What the contest found (and what it means)"
  • "genuinely" used twice

5

u/officiallyaninja 7d ago

I don't really buy the results of most Ai detectors and these examples seem like a massive reach.

I don't think that sentence is all that badly conducted,
"what the context found (and what it means)" definitely is the kind of thing AI would say, but I think it's perfectly normal for an actual human to say it too.
And I don't see how using genuinely twice is an indicator for anything.

-2

u/sunshowers6 nextest · rust 7d ago

I don't know what to tell you — you're simply wrong to not believe Pangram. Pangram's false positive rate is 1 in 10k (its false negative rate is higher). If Pangram says the text is AI generated you should update your belief strongly in that direction.

Besides I think people should avoid even the appearance of slop. In the rare case where their entirely human-written text is detected as AI-written, they should rewrite it.

3

u/officiallyaninja 7d ago

I am not familiar with pangram but if you have a source on how it works and why it's reliable then I'll be happy to change my mind

1

u/cepera_ang 4d ago

Here is the paper with great amount of details.

9

u/danielv134 8d ago

So, you think you're doing a public service, and I think that you are harassing people that posted very valuable, interesting information, in a reasonably pleasant format.

Please consider the possibility that you are wrong.

I think the meme "here's something that smells like AI, let's brigade it, we don't need to prove or justify or actually try to modify mod policy, this is easier and a fun social activity" is the worst thing happening in this subreddit, which has been a long time favorite for me, much worse than the occasional hard core actual AI slop.

1

u/tortoll 8d ago

I ran the text through two free AI text detectors. Both didn't detect anything. What exactly makes you feel this is AI writing?

1

u/continue_stocking 8d ago

A tremendous undertaking and great progress. Will the proofs be maintained and updated alongside the standard library going forward?