I would recommend trying Lean4 because I think it is better suited to programming. Lean has Rust-like toolchain manager; a build system (cf. `.agda-lib`); much more developed tactics (including `termination_by`/`decreasing_by`); more libraries (mathlib, and some experimental programming-oriented libraries for sockets, web, games, unicode...); common use of typeclasses in stdlib/mathlib; `unsafe` per declaration (cf. per module in Agda); sound opaque functions (which must have a nonempty return type) used for `partial` and ffi; "unchained" do-notation (early `return`, imperative loops with `break`/`continue`, `let mut`); easier (more powerful?) metaprogramming and syntax extensions. And in Agda you can't even use Haskell's type constructors with type classes (ex. monad polymorphic fns, and that makes it more difficult to make bindings to Hs libs, than to C libs in Lean).There are features in Agda/Idris (and probably Coq, about which I sadly know almost nothing) that are absent from Lean and are useful when programming (coinduction, set omega, more powerful `mutual`, explicit multiplicity, cubical? etc), but I'd say the need for them is less common.
No comments yet.