Hume is a functionally-based programming language developed at the University of St Andrews and Heriot-Watt University in Scotland, and named after the 18th Century philosopher David Hume. It targets real-time embedded systems, aiming to produce a design that is both highly abstract, yet which will still allow precise extraction of time and space execution costs, so allowing programs to be written that will execute under guaranteed bounded time and space constraints.
Hume is unusual in combining functional programming ideas with ideas from finite state automata. Automata are used to structure communicating programs into a series of "boxes", where each box maps inputs to outputs in a purely functional way using high-level pattern-matching. It is also unusual in being structured as a series of levels, each of which exposes different machine properties, which is highly unusual.
The Hume Design Model
The Hume language design attempts to maintain the essential properties and features required by the embedded systems ___domain (especially for transparent time and space costing) whilst incorporating as high a level of program abstraction as possible. It aims to target applications ranging from simple micro-controllers to complex real-time systems such as smartphones. This ambitious goal requires incorporating both low-level notions such as interrupt handling, and high-level ones of data structure abstraction etc. Of course such systems will be programmed in widely differing ways, but the language design should accommodate these varying requirements.
Hume is a three-layer language: an outer (static) declaration/metaprogramming layer, an intermediate coordination layer describing a static layout of dynamic processes and the associated devices, and an inner layer describing each process as a (dynamic) mapping from patterns to expressions. The inner layer is stateless and purely functional.
Rather than attempting to apply cost modeling and correctness proving technology to an existing language framework either directly or by altering a more general language (as with e.g. RTSJ), the approach taken by the Hume designers is to design Hume in such a way that formal models and proofs can definitely be constructed. Hume is structured as a series of overlapping language levels, where each level adds expressibility to the expression semantics, but either loses some desirable property or increases the technical difficulty of providing formal correctness/cost models.
Example
{- example file fibo-i.hume
-}
-- declarations
type Int = int 32 ;
exception EIncredible :: (Int, string) ;
exception EIllegalArgument :: string ;
-- expression language (eager evaluation)
fibo :: Int -> Int ;
fibo 0 = 1;
fibo 1 = 1;
fibo n = if n < 0 then raise EIllegalArgument "fibo: negative argument: " ++ (n as string)
else fibo (n-1) + fibo (n-2);
-- fibo bounded in time
bfibo :: Int -> Int ;
bfibo n = (fibo n) within 10ms ; -- restricted to 10 ms.
-- raises Timeout () (interpret only)
-- automata as stateless boxes
-- the state is kept by feedback into the mailboxes
box fib
-- tuple of inputs, single element mailboxes
in (n::integer, flag::integer)
-- type of the output with roles
out (nextn::integer, flag'::integer, result::(integer, integer, string))
-- within 500KB (400KB) -- heap and stack cost boundings (compiler only)
-- woud throw HeapOverflow, StackOverflow
handles Timeout, EIncredible, EIllegalArgument -- declares handled exceptions
match
-- pattern for the tuple of inputs -> expression_of_type_of_the_''out''_tuple
-- * wildcards for unfilled outputs, and unconsumed inputs
(n, 0) -> if n >= 99 then raise EIncredible (n, " reached")
else (n+1, 0, (n, bfibo n, "\n"))
| (n, 1) -> (n, 0, (n, *, " Timeout thrown\n"))
| (n, 2) -> (n, 0, (n, *, " EIncredible thrown\n"))
handle
-- exception_pattern -> expression_of_type_of_the_''out''_tuple
Timeout () -> ( 0, 1, (*, *, "Timeout caught, we restart n to 0\n"))
| EIncredible (n, msg) ->
(0, 2, (*, *, "Incredible: " ++ (n as string) ++ msg
++ ", we restart n to 0\n"))
| EIllegalArgument msg -> (0, 0, (*, *, "Ilegal argument: " ++ msg ++ "\n"))
;
-- connections
stream output to "std_out";
wire fib
-- fib ''in'' tuple match with origin mailboxes and sources
(fib.nextn initially 0, fib.flag' initially 0)
-- fib ''out'' tuple match with destination mailboxes and sinks
(fib.n, fib.flag, output)
;
External links
- The Hume Language Web Site
- The Hume Project at Heriot-Watt University
- Embedded Functional Programming in Hume
- The EmBounded project Project to certify resource-bounded code in Hume.
- Hume and Multicore