Hume and Poly

Owen Lynch

Mon May 08 2023

I just learned about Hume

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.

This aligns somewhat with my dreams for programming languages based on Poly, in that we should be thinking about programming in less powerful languages with more guarantees. It would be interesting to look more at Hume and understand whether parts of it could be formalized with Poly.