From: Hendrik Tews <tews@tcs.inf.tu-dresden.de>
> Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> writes:
> 
>    Note that void in C is definitely not zero. You cannot have variables
> 
> C++ standard, 3.9.1.9: The void type has an empty set of values. ...
> 
> So I would say void is zero. On the other side you have functions
> returning void. Therefore I would conclude that the type theory
> of C++ is unsound.

Which is almost the same thing as saying that the definition
contradicts itself...
My point was just that, looking at the way void is used in C, it
clearly does not have the usual proporties of zero, and among them the
fact no function should be able to return zero, or that all pointers
to void should be NULL.

For this reason it seems to me at first that the actual semantics of
void in C is that of (\exists a. a) aka unit (i.e. a value we know
nothing about), not that of (\forall a.a) aka zero (the impossibility).
You can safely cast any pointer to a void pointer, but not the
opposite. Additionaly, for representation reasons, you cannot copy or
allocate values of type void, so that they are non-existent in
practice, but this looks more like a consequence than a definition.
Another meaning of void seems to be the empty product, which again is
unit, with the extract constraint that you cannot store such a value
in C.

This is just my personal take on the question. I just don't think that
there is any serious model theory behind C's void, just a bunch of
practical constraints.

Jacques Garrigue