Hmm, I wonder how well would formal verification work with LLMs. I'm not really a fan of vibe coding, but the little I know about formal verification, it could very well work as a way how to prove your vibe-coded slop isn't shit.

I've looked into formal verification once few years ago, but it's too much math and thinking for me to grasp. If I remember it right, I guess the problem would be that you'd (or, LLM would, in this case) have to correctly describe the code in the formal verification language, and it would have to match 1:1 with the code, which is a point of failure? So we'd be back to square one, but instead of having to verify every single line of code, you'd have to check the proof. But maybe I'm wrong.

[–] Barracuda@lemmy.zip 2 points 2 hours ago

The LLM will just make up lies in the formal verification.

[–] rtxn@lemmy.world 52 points 13 hours ago* (last edited 13 hours ago) (1 children)

bcachefs

I don't know what Kent did, but I doubt it will surprise me at this point.

(edit) Fuck sake, Kent...

[–] Tm12@lemmy.ca 12 points 13 hours ago (1 children)

Appreciate the context from someone who doesn’t know Kent.

[–] Contramuffin@lemmy.world 42 points 12 hours ago (1 children)

Nothing serious, but he's well known for being impossible to work with. He has gotten into multiple arguments because he refuses to follow kernel development rules. When called out on it, he makes a big stink about it. Obviously his code doesn't get merged. Then he does the exact same thing again 1 month later.

He has gotten into multiple arguments with Linus Torvalds over his refusal to simply follow the kernel development rules. During those arguments he has made cheap shots at completely unrelated people, which then drags those people into the argument.

It's gotten to the point where apparently a significant portion of the kernel developers feel like he was negatively impacting the kernel, and Linus eventually removed his code from the kernel.

He's what you might call a Linux lolcow. And now he's doing even more lolcow things by... Getting weirdly attached to his LLM-sona

[–] yabbadabaddon@lemmy.zip 5 points 7 hours ago (1 children)

What is sad IMO is that he's quite freaking good. It's kind of a waste.

[–] MonkderVierte@lemmy.zip 2 points 2 hours ago

Then again, it's only a small gap between knowing you're good and megalomania. And he's the later.

[–] Scoopta@programming.dev 18 points 13 hours ago

Oh god, as if I wasn't scared enough about running a filesystem that got kicked out of mainline and is maintained more or less by a single dude. I'll stick to btrfs thanks

[–] hperrin@lemmy.ca 6 points 13 hours ago

Great article. That guy is legitimately being driven insane.