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.
A general programming discussion community.
Other programming communities: