this post was submitted on 23 Feb 2026
713 points (97.6% liked)

Technology

82000 readers
3648 users here now

This is a most excellent place for technology news and articles.

Our Rules

  1. Follow the lemmy.world rules.
  2. Only tech related news or articles.
  3. Be excellent to each other!
  4. Mod approved content bots can post up to 10 articles per day.
  5. Threads asking for personal tech support may be deleted.
  6. Politics threads may be removed.
  7. No memes allowed as posts, OK to post as comments.
  8. Only approved bots from the list below, this includes using AI responses and summaries. To ask if your bot can be added please contact a mod.
  9. Check for duplicates before posting, duplicates may be removed
  10. Accounts 7 days and younger will have their posts automatically removed.

Approved Bots

founded 2 years ago
MODERATORS
L3s@lemmy.world
enu@lemmy.world
technopagan@lemmy.world
L4s@lemmy.world
L3s@hackingne.ws
713
Car Wash Test on 53 leading AI models: "I want to wash my car. The car wash is 50 meters away. Should I walk or drive?" (opper.ai)
submitted 5 days ago by fubarx@lemmy.world to c/technology@lemmy.world
344 comments fedilink hide all child comments
 

Screenshot of this question was making the rounds last week. But this article covers testing against all the well-known models out there.

Also includes outtakes on the 'reasoning' models.

you are viewing a single comment's thread
view the rest of the comments
[–] bss03@infosec.pub 8 points 5 days ago* (last edited 5 days ago) (1 children)

Yeah, software is already not as deterministic as I'd like. I've encountered several bugs in my career where erroneous behavior would only show up if uninitialized memory happened to have "the wrong" values -- not zero values, and not the fences that the debugger might try to use. And, mocking or stubbing remote API calls is another way replicable behavior evades realization.

Having "AI" make a control flow decision is just insane. Especially even the most sophisticated LLMs are just not fit to task.

What we need is more proved-correct programs via some marriage of proof assistants and CompCert (or another verified compiler pipeline), not more vague specifications and ad-hoc implementations that happen to escape into production.

But, I'm very biased (I'm sure "AI" has "stolen" my IP, and "AI" is coming for my (programming) job(s).), and quite unimpressed with the "AI" models I've interacted with especially in areas I'm an expert in, but also in areas where I'm not an expert for am very interested and capable of doing any sort of critical verification.

[–] softwarist@programming.dev 2 points 4 days ago (1 children)

You might be interested in Lean.

[–] bss03@infosec.pub 3 points 4 days ago* (last edited 4 days ago) (1 children)

Yes, I've written some Lean. It's not my favorite programming language or proof assistant, but it seems to have "captured the zeitgeist" and has an actively growing ecosystem.

[–] softwarist@programming.dev 2 points 4 days ago (2 children)

Fair enough. So what are your favorites?

[–] bss03@infosec.pub 3 points 4 days ago

Right now, I'm spending more time in Idris. It's not a great proof assistant, but I think it's a lot easier to write programs in. Rocq is the real proof assistant I've used, but I don't have a strong opinion on them because all the proofs I've wanted/needed to write where small enough to need minimal assistance. (The bare bones features that are in Agda or Idris were enough.)

[–] bss03@infosec.pub 2 points 4 days ago* (last edited 4 days ago)

Also, my preference shouldn't matter to anyone else. If you want to increase your proof assistant skill (even from nothing), I suggest lean. Probably the same if you want to increase programming skill in a dependently typed language.

Honestly, I should get more comfortable with it.