[sondr3]

There's a small difference between type-level programming and type-driven programming, Idris does the latter while Rust the former (at least in my opinion). The library uses types to make illegal states impossible and therefore should qualify as type-level programming.

[mrkeen]

But there's no programming at the type level. The programming in the article is at the level of values (insofar as what is shown.).