No, a compiler (hell, a software) written in C is not correct, period. If you want a C compiler that has slight chances to be correct, you use compcert.
The small size is an awesome property for education (both for the writer and the reader). For this purpose, it's absolutely great, so kudos for that. :)
And also, we are seeing more and more certified C programs: see the DeepSpec NSF expedition grant, the Verified Software Toolchain, and the CertiKOS project for examples. I work with these guys.
Btw, hows progress coming on those projects? Specifically, are any of the tools (a) useful for non-experts with a little bit of training by tutorials, etc and (b) available for download in open-source or binary form yet? Thanks ahead of time.