Soon, I will be making available on this page the initial release of FunCC, a formally-verified, verifying and standards-compliant C compiler suite written in Haskell using the linear correctness principle originally described in my PhD thesis. In this project, I aim to implement a complete C compiler that is subject to stringent and formally-verified correctness guarantees, complies with the precise ANSI C89 and C99 standard specifications of the language, supports all known GNU C extensions, performs extensive optimisations of the generated programs and, last but not least, accommodates and aids formal reasoning about arbitrary correctness properties of the actual C programs being compiled, effectively answering Tony Hoare's grand challenge for computer science. Easy as a pie, eh? Well, these are the aims of the project, the actual expectations are somewhat more modest and, in reality, I intend FunCC to represent simply a bagful of pragmatic results from my research in the area of program translation. For the current status and progress, feel free to contact me by email. In the meantime, you can also download and play with the Haskell source developed as part of my original PhD research.