l4-ka, c++!

[M. Edward Borasky]

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 ..." :)

-- 
M. Edward (Ed) Borasky
mailto:znmeb at borasky-research.net
http://www.borasky-research.net
 
"Suppose that tonight, while you sleep, a miracle happens - you wake up
tomorrow with what you have longed for! How will you discover that a miracle
happened? How will your loved ones? What will be different? What will you
notice? What do you need to explode into tomorrow with grace, power, love,
passion and confidence?" -- L. Michael Hall, PhD