I believe you are correct. The advantage, on the other hand, is that you don't have to first acquire a PhD in mathematics and then learn Coq/Agda. Seriously though, simpler interfaces can add a lot of value, but only if the increase in ease of use makes up for the decrease in expressiveness.