Notes on Idris (2017)
Recently I talked with my cousin, who is also a software engineer, about dependent types, contract programming, invariants, and all that. Among other things I&#x27;ve told him about &quot;type-safe printf&quot; that you can write in Idris. He then asked me, why are there only purely functional languages with this feature. I had no actual answer.<p>So, does anybody know, why there still isn&#x27;t a &quot;C&#x2F;Go&#x2F;Java with dependent types&quot;? There is support for runtime checking via invariants in e.g. D, but no pre-compile-time checker.<p>Another question, is there (probably commercial) software that allows you to augment your code with invariant annotations and then check them as a pre-compilation step?