Idris VS pie

And here is a gist that demonstrates how simple it is to implement such a type-safe printf function:

https://github.com/mukeshtiwari/Idris/blob/master/Printf.idr

Pie, a dependently typed language for learning dependently typed programming

The computer scientists who are figuring these things out are constructing the tools that software engineers need; just like the mathematicians who developed calculus and the physicists who extended Newtonian mechanics into something engineers can apply. Just as an engineer's tools and materials are calculus and physics (not hammers or concrete and steel), a software engineer's tools and materials are proof-assistants, category theory, linear polarized logic, and dependent type theory (not the Rust programming language or the UNIX platform).

That's basically this[0] book, is it not?

[0] https://thelittletyper.com

I really should read https://thelittletyper.com/

It lets you create languages like Pie which is designed to teach others about dependent types:

https://thelittletyper.com/

Yep, this is one possibility - an example is the language pie from the book The Little Typer. But my claim was not that there are no expressions for types, just that declarations aren't expressions.