undefined | Better HN

0 pointsepgui3y ago0 comments

Agda and Idris both also position themselves similarly.

0 comments

2 comments · 1 top-level

siknad3y ago· 1 in thread

Lean4 is intended to be both, while Idris is more on the programming side and Agda - one the proof side. Maybe I'm mistaken about Idris, but Agda really doesn't prioritize programming: library handling, ffi, and tooling are all rudimentary.

epguiOP3y ago

You may be right— My knowledge of these languages does not run very deep (although I am enthusiastic about them and am learning).

j / k navigate · click thread line to collapse