A programming language called Safe is the topic of this paper. It has the syntax and operational semantics of a standard functional language, but is limited to first-order functions.

Safe adds some simple annotations to do with memory management to functional programming. There is one that ensures that a value passed to a function is a copy rather than an alias of an existing structure, and another that states that a structure passed to a function should be destroyed. Together, these enable much tighter control of memory usage than is possible with conventional functional programming.

The annotations that would be used by a Safe programmer are translated to a more complex form of annotation (using the concept of a region-based memory management system), and this in turn translates to imperative code for a virtual machine.

The bulk of the paper is taken up by a description of the translation process and the syntax and semantics of the languages. Detailed formal proofs of the properties of the languages are given.

The overall aim is to enable functional-style programming, but without the uncertainty in timing caused by automatic garbage collection, and with a more efficient use of memory, suitable for use on devices that have strict memory requirements.

This is a useful development of ideas, demonstrating that there are plenty of new fundamental ideas in programming languages that need to be explored.