Scrap your Haskell! Hume is here

Since the focus of the Hume design is on dependable applications (such as safety critical or embedded systems), it is paramount that Hume programs have predictable and, preferably, provable properties. However, the strong properties of program equivalence, termination and time and space use are undecidable for Turing computable languages. Conversely, languages in which such properties are decidable (i.e. finite state machines) lack expressiveness. The goal of the Hume language design is to support a high level of expressive power, whilst providing strong guarantees of dynamic behavioural properties such as execution time and space usage.

We identify a series of overlapping Hume language levels, where each level adds expressibility to the expression semantics, but either loses some desirable behavioural property or increases the technical difficulty of providing formal correctness/cost models. These levels are:

HW-Hume: a hardware description language — capable of describing both synchronous and asynchronous hardware circuits, with pattern matching on tuples of bits, but with no other data types or operations [27];
FSM-Hume: a hardware/software language — HW-Hume plus first-order functions, conditionals expressions and local definitions [26];
Template-Hume: a language for template-based programmimng — FSM-Hume plus predefined higher-order functions, polymorphism and inductive data structures, but no user-defined
higher-order functions or recursive function definitions;
PR-Hume: a language with decidable termination — Template-Hume plus user-defined primitive
recursive and higher-order functions, and inductive data structure definitions;
Full-Hume: a Turing-complete language — PR-Hume plus unrestricted recursion in both functions and data structures.

http://www.hume-lang.org/

Here's a bit adder:

-- full adder as half adders and or

type Bit = int 1;

box gen
in (t::int 64)
out (t'::int 64,x,y,c::Bit)
match
0 -> (1,0,0,0) |
1 -> (2,0,1,0) |
2 -> (3,1,0,0) |
3 -> (4,1,1,0) |
4 -> (5,0,0,1) |
5 -> (6,0,1,1) |
6 -> (7,1,0,1) |
7 -> (0,1,1,1);

template half2
in (x,y::Bit)
out (s,c::Bit)
match
(0,0) -> (0,0) |
(0,1) -> (1,0) |
(1,0) -> (1,0) |
(1,1) -> (0,1);

instantiate half2 as h * 2;

box or
in (x,y::Bit)
out (z::Bit)
match
(0,0) -> 0 |
(0,1) -> 1 |
(1,0) -> 1 |
(1,1) -> 1;

box show
in (s,c::Bit)
out (sc::(Bit,Bit,char))
match
(s,c) -> (s,c,'\n');

stream output to "std_out";

wire gen (gen.t' initially 0) (gen.t,h1.x,h1.y,h2.x);
wire h1 (gen.x,gen.y) (h2.y,or.x);
wire h2 (gen.c,h1.s) (show.s,or.y);
wire or (h1.c,h2.c) (show.c);
wire show (h2.s,or.z) (output);