Hello.
Back at FOSDEM meeting, I mentioned again that nowadays, writing an
operating system in C is IMHO a horrible idea. So many of the mistakes C
makes easy simply should not occur any more. Unfortunately, I have not been
able to find a language that could satisfactorily replace C, even if some
have tried.

To join in the fray of futile attempts of making operating systems better,
I decided to design and implement a language with which I would be
comfortable writing a core TCB of an OS. Obviously, I don't expect HelenOS
to be rewritten in a different language, but I'd appreciate input of people
on this list.

What follows is a list of basic requirements and current direction:


Requirements:
 - strong static typing, compiled to native code
 - ability to statically prove absence of invalid dereferences,
   integer overflows, out of bounds array accesses... any condition that
would cause
   the program to misbehave
 - similar to C (superficially, and in simplicity)
 - minimal requirements for runtime support
   - programs without dynamic memory must be possible
 - ability to call functions written in assembly/C
 - ability to write assembly inline and do check it (i.e. not just "put
this string in the generated code")
 - builtin support for asynchronous code (fibrils) and tools to provably
avoid races in SMP environment

Extending from above (mostly my preferences):
 - arbitrary ranges instead of fixed machine types; the compiler will check
that the range can't overflow (as in Ada)
 - owned, borrowed and managed pointers (as in Rust)
 - statement-based syntax, packages (as in Go)
 - parser plugins for machine code
 - contracts (preconditions, postconditions, invariants)
   - statically verified (on a function level - a method call is specified
by its interface, no inlining)
   - integration with exchangable SMT solver (SMT-LIB 2.0 provides suitable
interface)
   - (for an example see Dafny)
 - no classes, statically bound methods, type-tagged interface pointers to
provide dynamic binding (as in Go)
 - dynamic stack size, unless the maximum can be determined statically
(also Go)
 - compiled (at least) to ANSI C



Based on my current idea about syntax and functionality, I am about halfway
done with a basic interpreter (alas with none of the static checking).
What are your ideas? What would you require from the perfect language for
writing a kernel and stuff around it?

Cheers,
-- Jirka Z.
_______________________________________________
HelenOS-devel mailing list
[email protected]
http://lists.modry.cz/listinfo/helenos-devel

Reply via email to