▲ 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 (4 children) You might be interested in Lean. permalink fedilink source parent hideshow 4 child comments replies: [–] bss03@infosec.pub 3 points 8 months ago (3 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. permalink fedilink source parent hideshow 3 child comments replies: [–] 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 (3 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. permalink fedilink source parent hideshow 3 child comments replies: [–] 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
[–] 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