Hi William,
As you are compiler experts, I am asking your help. You may overestimate our compiler skills :)
If somebody is interested in functional programming and in formal methods to help to implement a verified compiler , he is welcome :) I saw you giving out a list of sources in the haskell mailing list as well, however you missed:
Haskell also depends on a complicated run-time system. Such run-time systems are often unverified. Implementing a minimal, high-assurancerun-time system is a topic for future work. The runtime for Yhc is relatively simple - probably the simplest and cleanest of any of the Haskell implementations. The compiler is
Catch: http://www-users.cs.york.ac.uk/~ndm/projects/catch.php ESC/Haskell: http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps [Note, I am the one who does Catch, so considered that a biased plug] probably not a good start to build a high assurance system :) Thanks, and good luck! Neil