[JadeNB]

> I've always thought that a language like Idris based on Dependent Types would by far be the best language for this.

As someone who loves the idea of dependent types, it seems to me that this is the best theoretical solution, but maybe not the best practical solution. If solving a simple-seeming domain problem involves modelling, not just first-order types, but the whole theory of dependent types, then I think people are going to start looking for escape hatches rather than upgrading their mental models.