I enjoy pedantry too, so I guess I kind of understand why you keep making this point. However, it's not relevant to what the OP asked, which was about the math

I enjoy pedantry too, so I guess I kind of understand why you keep making this point. However, it's not relevant to what the OP asked, which was about the mathematical modeling of C functions that return void, rather than trivia related to C syntax. In the two positions in C and C++ that I discussed, the domain and codomain of a function, void is functionally identical to unit, despite your protestations to the contrary (there is literally no semantic distinction between them). In Rust, none of these restrictions exist and we can freely use unit in all the ways you described, but in the domain and codomain of a function it still works just like void does in C (we can't cast from arbitrary types to void, but this is more because Rust takes a hard stance against stupid casts than because it would be difficult to implement, and it has other ways of representing deliberately throwing away a value). The C standard, of course, may disagree, and claim that there is no value of type "void" and that void functions "have no return type." That I can call and successfully return from a void function, call a function taking void, and even cast a value to void, provide ample evidence (which would also be backed up by reading the standard) that what it means by "type" is not the same thing as what a mathematician means by "type" (and "completed" is a complete red herring here). The fact that you don't explicitly return a void value doesn't really mean anything--no return or return with no value are pure syntactic sugar for returning a void value, which is also how it's implemented in many other languages that enjoy explicit unit types. What I can't do in C is bind one of the many values of type void to a variable (and do a few other things, like call `sizeof` on the type, or explicitly name the inhabitant of void as a literal, which again have pretty much nothing to do with the semantics of the thing). That is a much weaker restriction, for the same reason that defining a binding as `const` is much weaker than a guarantee that the underlying value isn't mutated; bindings are a largely syntactic artifact and don't affect the mathematical model of a C function in any way. This is especially true for unit types, since having an instance of one is completely uninformative as they both always exist and are all definitionally equal! Of course, this doesn't apply to void * , which as you point out is really its own bizarre thing that is mostly unrelated to void itself (I'd like to call it a pointer to the top type, but I'm not certain even that would cover its semantics). I think it's fair to say that despite some degree of overlap, void * is an unrelated concept overloading the "void" keyword, and that the actual interpretation of bare "void" is indeed equivalent to unit, not that every other use of `void` in C is completely arbitrary and unprincipled. The reason, AFAIK, why C doesn't just add all those void-related features it's missing is because it has baked in decisions like "every type has a nonzero size" and "arrays are pointers" (conflicting with void * ) that make adding stuff like this after the fact very complicated, not because it wouldn't make sense semantically (in a proper semantic model, where void * was called something like any * and zero sized types were legal, many of these issues would go away, including--I'm pretty sure--all the reasons why C and C++ must insist that void values not be completed). In any case, none of this helps with or is relevant to reasoning about C functions as mathematical objects. And just to be extra clear--even if C had no keyword at all for `void` functions and didn't have `void` as an option for argument lists, these functions would still be modeled as taking / returning values of type unit.