▲ 705 ▼ 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 8 months ago by fubarx@lemmy.world to c/technology@lemmy.world 322 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.
[–] softwarist@programming.dev 2 points 8 months ago (2 children) Fair enough. So what are your favorites? permalink fedilink source parent hideshow 2 child comments replies: [–] bss03@infosec.pub 3 points 8 months 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.) permalink fedilink source parent [–] bss03@infosec.pub 2 points 8 months ago* (last edited 8 months 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. permalink fedilink source parent
[–] bss03@infosec.pub 3 points 8 months 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.) permalink fedilink source parent
[–] bss03@infosec.pub 2 points 8 months ago* (last edited 8 months 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. permalink fedilink source parent