Post #513090
2026-02-25 04:28 UTC
Fair enough. So what are your favorites?
Replies (2)
-
@bss03@infosec.pub 2026-02-25 05:02
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 2026-02-25 05:07
Also, my preference shouldn’t matter to anyone else. If you want to increase you 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.