I'm happy this exists, and that Agda has the facilities to make it feasible, but sad that automated formal systems are so primitive compared to software develop

I'm happy this exists, and that Agda has the facilities to make it feasible, but sad that automated formal systems are so primitive compared to software development tools. Is this gap just lack of motivation for more people to contribute, or the culture of formal systems, or some source of technical barriers, or ??