[afiori]

In the field of formal type systems two common approaches to defining types, in practice they are quite similar but in my opinion they differ a lot in framing.

One side can be represented by Haskell, Hindley–Milner type systems, or even Coq; here every value has its own "best" type that is intrinsecally associated with it, that is values and types are defined and constructed together.

On the other side you have sort of a formal definition of duck-typing; you have values and properties that are satified by some set of values, here you have your values (all numbers, all strings, all memory addresses) and expres in usual logic terms any property you want (e.g. this memory address must be either Null or point to a string of even length).

All this to say that C has a nice type system from the first point of view (function pointer allow you to have higher order functions!) but a very weak one from the second point of view in that it is very hard to decide if an operation will have a valid result just by the types of the values you feed into it (let's not talk about UB for now).

In my opinion in later decades there is a movement to care more about type systems that follow the second approach. In my opinion it is one of the reason for the success of Typescript; its objective wasn't to have a nice type system full of good properites, but to model how javascript was being written.