Agda's been around for 24 years, according to Wikipedia, and it hasn't exactly revolutionized software development: I'm not aware of any notable software written in it, or of anyone so much as winning a programming competition while using it (and some of those are designed to promote functional programming) So, frankly, I'm skeptical that Agda's trade-offs in the performance-convenience-correctness space are good.