Agda if you want to write proofs, Idris if you want to write programs. There is also Coq which is more popular but I would not suggest it to a beginner. (note:

Agda if you want to write proofs, Idris if you want to write programs. There is also Coq which is more popular but I would not suggest it to a beginner. (note: both Agda and Idris can be used for both proofs and programs, it's just that each have their own focus)