Thanks!! I'm just getting into this L4 / Hurd game. My main concern isn't efficiency -- I leave the speed issues to the folks who give us a 2X clock frequency boost every 18 months. :) My concerns are correctness and stability of the OS, and various project management issues like predictability and stability of dates, interfaces and specifications, production of accurate and usable documentation, etc. I'm by no stretch of the imagination a competent C++ programmer; I can just barely read C++ once the object-oriented features show up.
In my trolling about, I discovered that the Fiasco folks have put some effort into "correctness proofs" of Fiasco. See the Vfiasco site
http://os.inf.tu-dresden.de/vfiasco/
How difficult would it be to shift this effort from Fiasco to Pistachio? How difficult would it be to port DROPS and friends
http://os.inf.tu-dresden.de/drops/
from Fiasco to Pistachio? I'm interested in both tracks -- a real-time operating system and a general-purpose Linux-like desktop and server system. "One OS to rule them all ..." :)