The Hume Project at Heriot-Watt University

Hume - Higher-order Unified Meta-Environment

0. Project Name

The Hume project ran from around 2000 to 2013. The name was chosen to mark the skeptical philosophy of the highly influential Scottish Enlightenment philosopher David Hume. Hume was a racist and engaged in slavery. Had we been aware of this, we would not have chosen his name.
(added 14/9/20)

1. Introduction

This page provides information about and links to Hume activity at Heriot-Watt University within the Dependable Systems Group. The wider Hume project home page is here.

Hume is a novel programming language, intended for resource bounded domains, designed at Heriot-Watt University and the University of St Andrews. It is based on concurrent finite state automata controlled by pattern matching and recursive functions over rich types. Hume has been designed as a multi-level language, where different levels have different formal properties amenable to different analyses. HW-Hume is a relatively impoverished language of bits and tuples for characterising hardware, with decidable equivalence and termination, and predictable time and space behaviour. FSM-Hume introduces fixed precision abstractions over bit tuples, including integers, reals, strings and vectors, with associated operators and conditional constructs. This level, oriented to wider finite state machine-based designs, has strongly bounded time and space behaviour. HO-Hume augments FSM-Hume with a repertoire higher-order function with known cost models, such as map and fold, and user-defined non-recursive functions. PR-Hume extends HO-Hume with user-defined primitive recursive bounded functions and full Hume is a Turing Complete language.

Active areas of research include: the development of characterisation, time and space analyses for the different levels; the elaboration of a semantics-preserving refinement methodology from higher to lower levels, to improve the accuracy of costing; native code compilation for PC and embedded use; applications in image and vision processing, and control.

Current Hume implementations include a reference interpreter, available below, and an abstract machine with associated compiler. Current Hume costing tools include space analysers for HW-, FSM- and PR-Hume.

2. People

Dr Abyd Al Zain RA, Islay project
Dr Norman Scaife RA, EmBounded project
Gudmund Grov, RA, EmBounded Project/PhD student, Integrating model checking and proof for Hume.
Robert Pointon, RA, EmBounded project (2005-7)
Dr Zezhi Chen, RA, SEAS project (2005-7)