The Benefits and Costs of Writing a POSIX Kernel in a High-Level Language