It is weird to me that so many people are getting caught up on the fact that type safe printf has been around forever. If someone has looked into Idris they almost certainly know that it isn't a new concept.

I linked it because its implementation is amazing comparatively and it is just one clean example of what is possible.