Idris2 feels right. The installation is easy (Chez Scheme backend, Node.js backend should be even easier)
And it’s snappy now.
The slogan is “Type driven development”, Edwin Brady’s presentation is really impressive.
Agda is for mathematics, Idris2 focus is on resource management and performance.
I did a workshop with Dr Brady and it was great, I highly recommend attending to his talks.