[Pl-seminar] 11/10: Mark P. Jones, "Habit: A Functional Language for Bare-metal Programming"

[Vincent St-Amour]

NEU Programming Languages Seminar presents

Mark P. Jones
The High Assurance Systems Programming Project (HASP)
Department of Computer Science
Portland State University, Portland, Oregon

*** NOTE: Non-Standard Time ***
Thursday, 11/10

11:00am - 1:00pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Habit: A Functional Language for Bare-metal Programming

Several years ago, our group at Portland State began to explore the
"crazy notion" of using Haskell---a high-level, purely functional
language---for the development of operating systems components.
This led to the development of a proof-of-concept demonstration
system called "House", and more recently to a version of the L4
microkernel, both implemented primarily in Haskell.  The results
were encouraging, but also highlighted some weaknesses of Haskell in
this particular domain, including not only the expected performance
issues, but also the reliance on a large runtime system, and some
difficulties in providing precise types for key low-level
operations.

In this talk, we present the Habit programming language ("Haskell"+
"bits"), which is inspired by Haskell, but designed more
specifically to support the construction of bare-metal software.
The overall design is fairly conservative---we have attempted to
retain much of the familiarity and usability of Haskell---but we
have also tried to address some of the weaknesses that we
encountered in our earlier work.  Like Haskell, for example, Habit
provides strong support for both functional and imperative styles of
programming.  But it also differs by adopting a strict evaluation
model, and by introducing new language features that include:
mechanisms for fine control over representation of bit-level and
memory-based data structures; a novel approach to initialization of
memory areas; and a type system that allows precise characterization
of size and layout information via type level naturals.

The talk will also describe the status of our prototype
implementation, a novel aspect of which is the use of Leroy et al.'s
Compcert framework in the backend as a step towards a long term goal
of supporting certifying compilation of high-assurance, bare-metal
software systems.