You are right and it seems you have a very good gut-feeling about these things! :) What you describe is commonly called a "(value) dependent type system". Ther

You are right and it seems you have a very good gut-feeling about these things! :) What you describe is commonly called a "(value) dependent type system". There are languages that support this, e.g. Idris which was specifically built for that: https://www.idris-lang.org/ https://www.idris-lang.org/ Here is an example where the printf function is built purely in Idris: https://paulosuzart.github.io/blog/2017/06/18/dependent-types-and-safer-code/ https://paulosuzart.github.io/blog/2017/06/18/dependent-type... The compiler will parse the input string such as "some number %d and a string %s" at compile time (!) and assess whether the following arguments passed to printf satisfy the shape of the string.