Public interfaces should ideally be formally typed, both to provide a behavioral contract between parties and to serve as user documentation. Whether the contra

Public interfaces should ideally be formally typed, both to provide a behavioral contract between parties and to serve as user documentation. Whether the contract is enforced at compile- or run-time is secondary to having a formal mechanism for expressing it in the first place; ditto whether the code hidden behind those interfaces is explicitly typed, inferred, or untyped. Two problems that tend to occur in practice: * Untyped languages (e.g. Python, Ruby, JavaScript) typically lack a formal dialect for expressing parameter and result types, and most don’t even provide formal mechanism for annotating interfaces. Without a common language for expressing interface types, it’s nigh impossible to develop the tooling and education that are the necessary prerequisites to popular adoption. * Typed languages (e.g. C†, Java, Swift) frequently have poor/limited expressivity, creating friction for users, who end up fighting against the type system instead of working with it to describe their precise needs, while failing to provide the promised safety. e.g. Inability to describe numeric bounds means many functions with integer/double parameters will be partial, and passing inappropriate values will trigger runtime errors/aborts/undefined behaviors (e.g. divide-by-zero, bad array index). And that’s just the easy stuff. Python3 is one exception to the former, in that function interfaces can be formally annotated, though the language itself doesn’t provide the mechanism to enforce those annotations. And Eiffel is something of an exception to the latter in that interfaces are annotated with a mix of compile- and run-time checks. And then, of course, there’s ongoing work on dependent type systems and no doubt other CS research that may someday filter down into the production languages in mainstream use. But it’s tough and slow, and a giant wildly-inconsistent ballache in the meantime, with more really badly reinvented wheels than it’s possible to count. -- † Inasmuch as C can be said to have a “type system” at all (Really, it’s just got a handful of annotations for allocating memory on stack.)