[m_j_g]

It is nice to see practical application of dependently typed language!

[dwohnitmok]

Looking through the GitHub repo it doesn't look to actually use any of the dependently typed features of Idris.

(And I see now at the end of the article that they mention this).

If this grows in the future, I'd be curious to see if the team starts to integrate any dependent types.