C++ Truths

Just a few days ago I came across an intriguing blog-post  about type-safe printf using dependent typing. The blog-post has since become inaccessible and therefore, I've copied an excerpt here. I want to thank Zesen Qian for publishing this blog-post. .... printf  originated from the C programming language and has been a headache since then because a proper call of  printf  requires the number and types of arguments to match the format string; otherwise, it may visit a wild memory or a wrong register. In recent versions of GCC this issue is addressed by type checks hard coded into the compiler itself, which is ugly because the compiler should not be caring about the safety of applications of a specific function.... The key issue here is that, considering the curried version, the type of the returned function of applying the format string to  printf , actually depends on the value of that format string. That is to say,  printf "%s" : String -> Str...