<p>Linear types and separation logic are both great, but can require quite a bit of programmer effort. Writing a safe linked list in Rust could be pretty hard, for instance.</p>

<p>But there is an alternative that requires much less programmer effort, although with less strict guarantees. A (pretty old) stream of work is to guarantee memory safety by using (usually a stack of) regions. Using region inference, a compiler can statically decide which region a piece of allocated data should go into, and deallocate the region when it goes out of scope. </p>

<p>Region inference is provably safe (can't deallocate reachable memory) and requires minimal programmer interference, but it is not "total" (i.e. it still can leak memory, although definitely much better than "do nothing"), so it's usually combined with GC in practice. The <del>MLton</del> ML Kit compiler uses regions to eliminate most GC calls, but it still has a GC because it would still leak memory otherwise. According to some of the early pioneers on regions, region inference wasn't actually invented for this purpose (it was for automatic parallelization, I think); but it just turned out it could be used for memory management as well.</p>

<p>For a starting point, I would say go for the paper "Implementation of the Typed Call-by-Value λ-calculus using a Stack of Regions" by Mads Tofte and Jean-Pierre Talpin. For more papers on region inference, look for other papers by M. Tofte and J.-P. Talpin, some of Pierre Jouvelot's work, as well as Greg Morrisett, Mike Hicks, and Dan Grossman's series of papers on Cyclone.</p>

CC BY-SA 4.0
2018-10-23T23:24:41.983Z
2018-10-25T04:48:03.713Z
2018-10-25T04:48:03.713Z
xrq
<p>A trivial scheme for the "bare metal" systems is to simply disallow all runtime memory allocations. Remember, even the C <code>malloc/free</code> pair requires a runtime library. But even when all objects are defined at compile time, they can be defined in a typesafe way.</p>

<p>The chief problem here is the fiction of immutable values in pure functional languages, which are created while the program runs. Real hardware (and certainly bare metal systems) rely on mutable RAM, which is in limited supply. The runtime of a functional language implementation in practice dynamically allocates RAM as new "immutable" values are created, and garbage collects them when the "immutable" value is no longer needed.</p>

<p>And for most interesting problems, the lifetime of at least some values depends on runtime (user) input, so lifetimes can't be statically determined. But even if the lifetime doesn't depend on input, it can be highly non-trivial. Take the simple program repeatedly finding primes simply by checking every number in order, checking against all primes up to <code>sqrt(N)</code>. Clearly this needs keeps the primes and can recycle the memory used for the non-primes. </p>

CC BY-SA 3.0
2018-01-22T13:36:17.543Z
2018-01-22T13:36:17.543Z
MSalters
<p>Roughly speaking, there are two main strategies for safe manual memory management. </p>

<ol>
<li><p>The first approach is to use some substructural logic like linear logic to control resource usage. This idea has floated around basically since linear logic's inception, and basically works on the observation that by banning the structural rule of contraction, every variable is used at most once, and so there is no aliasing. As a result, the difference between in-place update and re-allocation is invisible to the program, and so you can implement your language with manual memory management.</p>

<p>This is what Rust does (it uses an affine type system). If you are interested in the theory of Rust-style languages, one of the best papers to read is Ahmed et al's <a href="http://www.ccs.neu.edu/home/amal/papers/linloc-fi07.pdf" rel="noreferrer">L3: A Linear Language with Locations</a>. As an aside, the LFPL calculus Damiano Mazza mentioned is also linear,  has a full language derived from it in the <a href="http://www.raml.co/" rel="noreferrer">RAML language</a>. </p>

<p>If you are interested in Idris-style verification, you should look at Xi et al's <a href="http://www.ats-lang.org/" rel="noreferrer">ATS language</a>, which is a Rust/L3 style language with support for verification based on Haskell-style indexed types, only made proof-irrelevant and linear to give more control over performance. </p>

<p>An even more aggressively dependent approach is the <a href="https://www.fstar-lang.org/" rel="noreferrer">F-star language</a> developed at Microsoft Research, which is a full dependent type theory. This language has a monadic interface with pre- and post-conditions in the spirit of Nanevski et al's <a href="http://ynot.cs.harvard.edu/papers/jfpsep07.pdf" rel="noreferrer">Hoare Type Theory</a> (or even my own  <a href="https://www.cl.cam.ac.uk/~nk480/dlnl-paper.pdf" rel="noreferrer"><em>Integrating Linear and Dependent Types</em></a>), and has a defined subset which can be compiled to low-level C code -- in fact, they are shipping verified crypto code as part of Firefox already!</p>

<p>To be clear, neither  F-star nor HTT are linearly-typed languages, but the index language for their monads are usually based on Reynold and O'Hearn's <a href="https://www.cs.cmu.edu/~jcr/seplogic.pdf" rel="noreferrer"><em>separation logic</em></a>, which is a substructural logic related to linear logic that has seen great success as the assertion language for Hoare logics for pointer programs.</p></li>
<li><p>The second approach is to simply specify what assembly (or whatever low level IR you want) does, and then use some form of linear or separation logic to reason about its behaviour in a proof assistant directly. Essentially, you can use the proof assistant or dependently-typed language as a very fancy macro assembler that only generates correct programs. </p>

<p>Jensen et al's <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/hlsl.pdf" rel="noreferrer"><em>High-level separation logic for low-level code</em></a> is a particularly pure example of this -- it builds separation logic for x86 assembly! However, there are many projects in this vein, like the <a href="http://vst.cs.princeton.edu/" rel="noreferrer">Verified Software Toolchain</a> at Princeton and the <a href="http://flint.cs.yale.edu/certikos/" rel="noreferrer">CertiKOS</a> project at Yale.</p></li>
</ol>

<p>All of these approaches will "feel" like a bit like Rust, since tracking ownership by restricting the usage of variables is key to them all. </p>

CC BY-SA 3.0
2018-01-22T17:33:48.820Z
2018-01-22T17:33:48.820Z
Neel Krishnaswami
<p>Let's say we wanted a typeful, pure functional programming language, like Haskell or Idris, that is aimed at systems programming without garbage collection and has no runtime (or at least not more than the C and Rust "runtimes"). Something that can run, more or less, on bare metal.</p>

<p>What are some of the options for static memory safety that don't require manual memory management or runtime garbage collection, and how might the problem be solved using the type system of a pure functional similar to Haskell or Idris?</p>

CC BY-SA 3.0
2018-01-21T15:07:17.037Z
Are you saying that you'd like the types in the language to serve as a way of avoiding garbage collection? The basic problem arises in evaluation of functions. A function is evaluated to a closure, which encapsulates the current runtime environment. That is the major source of having to do garbage collection. Unless you change the typing rule for functions, I don't see how types are going to help with this. Java and other languages with broken $\lambda$-abstractions get aroudn this by mutliating the formation of closures: they disallow references that would require gabrage collection.
Andrej Bauer
CC BY-SA 3.0
2018-01-21T17:21:54.607Z
Surely Rust had to address the same problem of function evaluation and closures with its ownership model and borrow checker? Memory management just means knowing how long the values are alive, what other values depend on them, and destroying unused values when they're dead, right?

So I guess I'm really asking whether memory management could be encapsulated in a set of types that can be checked for correctness through the type system, without extending the basic machinery of the language or compiler by adding a whole new ownership system and "borrow checker" (which is Rust's way).
analogyschema
CC BY-SA 3.0
2018-01-22T07:21:19.423Z
What about Martin Hofmann's [LFPL](https://pdfs.semanticscholar.org/2fcc/9b18731f8f96eca9a3bc6855cb66a7f0d66f.pdf)?  It has a special base type, the "diamond", on which a linear type discipline is enforced, allowing types to account for basic memory usage (allocation/deallocation).  Would that go in the direction you are talking about?
Damiano Mazza
<pl.programming-languages><language-design>
Type-based memory safety without manual memory manage or runtime garbage collection?
analogyschema
# Type-based memory safety without manual memory manage or runtime garbage collection?

(Asked by: username_0 on 2018-01-21)

Let's say we wanted a typeful, pure functional programming language, like Haskell or Idris, that is aimed at systems programming without garbage collection and has no runtime (or at least not more than the C and Rust "runtimes"). Something that can run, more or less, on bare metal.

What are some of the options for static memory safety that don't require manual memory management or runtime garbage collection, and how might the problem be solved using the type system of a pure functional similar to Haskell or Idris?

**Tags:** pl.programming-languages, language-design
> **Comments:**
> **username_1**: Are you saying that you'd like the types in the language to serve as a way of avoiding garbage collection? The basic problem arises in evaluation of functions. A function is evaluated to a closure, which encapsulates the current runtime environment. That is the major source of having to do garbage collection. Unless you change the typing rule for functions, I don't see how types are going to help with this. Java and other languages with broken $\lambda$-abstractions get aroudn this by mutliating the formation of closures: they disallow references that would require gabrage collection.  
> **username_0**: Surely Rust had to address the same problem of function evaluation and closures with its ownership model and borrow checker? Memory management just means knowing how long the values are alive, what other values depend on them, and destroying unused values when they're dead, right?  So I guess I'm really asking whether memory management could be encapsulated in a set of types that can be checked for correctness through the type system, without extending the basic machinery of the language or compiler by adding a whole new ownership system and "borrow checker" (which is Rust's way).  
> **username_2**: What about Martin Hofmann's [LFPL](https://pdfs.semanticscholar.org/2fcc/9b18731f8f96eca9a3bc6855cb66a7f0d66f.pdf)?  It has a special base type, the "diamond", on which a linear type discipline is enforced, allowing types to account for basic memory usage (allocation/deallocation).  Would that go in the direction you are talking about?  

---

## 3 answers

### Answer by username_5 on 2018-01-22. Score: 24 | Accepted answer

Roughly speaking, there are two main strategies for safe manual memory management.

1. The first approach is to use some substructural logic like linear logic to control resource usage. This idea has floated around basically since linear logic's inception, and basically works on the observation that by banning the structural rule of contraction, every variable is used at most once, and so there is no aliasing. As a result, the difference between in-place update and re-allocation is invisible to the program, and so you can implement your language with manual memory management.

   This is what Rust does (it uses an affine type system). If you are interested in the theory of Rust-style languages, one of the best papers to read is Ahmed et al's [L3: A Linear Language with Locations](http://www.ccs.neu.edu/home/amal/papers/linloc-fi07.pdf). As an aside, the LFPL calculus Damiano Mazza mentioned is also linear, has a full language derived from it in the [RAML language](http://www.raml.co/).

   If you are interested in Idris-style verification, you should look at Xi et al's [ATS language](http://www.ats-lang.org/), which is a Rust/L3 style language with support for verification based on Haskell-style indexed types, only made proof-irrelevant and linear to give more control over performance.

   An even more aggressively dependent approach is the [F-star language](https://www.fstar-lang.org/) developed at Microsoft Research, which is a full dependent type theory. This language has a monadic interface with pre- and post-conditions in the spirit of Nanevski et al's [Hoare Type Theory](http://ynot.cs.harvard.edu/papers/jfpsep07.pdf) (or even my own [*Integrating Linear and Dependent Types*](https://www.cl.cam.ac.uk/~nk480/dlnl-paper.pdf)), and has a defined subset which can be compiled to low-level C code -- in fact, they are shipping verified crypto code as part of Firefox already!

   To be clear, neither F-star nor HTT are linearly-typed languages, but the index language for their monads are usually based on Reynold and O'Hearn's [*separation logic*](https://www.cs.cmu.edu/~jcr/seplogic.pdf), which is a substructural logic related to linear logic that has seen great success as the assertion language for Hoare logics for pointer programs.
2. The second approach is to simply specify what assembly (or whatever low level IR you want) does, and then use some form of linear or separation logic to reason about its behaviour in a proof assistant directly. Essentially, you can use the proof assistant or dependently-typed language as a very fancy macro assembler that only generates correct programs.

   Jensen et al's [*High-level separation logic for low-level code*](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/hlsl.pdf) is a particularly pure example of this -- it builds separation logic for x86 assembly! However, there are many projects in this vein, like the [Verified Software Toolchain](http://vst.cs.princeton.edu/) at Princeton and the [CertiKOS](http://flint.cs.yale.edu/certikos/) project at Yale.

All of these approaches will "feel" like a bit like Rust, since tracking ownership by restricting the usage of variables is key to them all.


---

### Answer by username_3 on 2018-10-23. Score: 4

Linear types and separation logic are both great, but can require quite a bit of programmer effort. Writing a safe linked list in Rust could be pretty hard, for instance.

But there is an alternative that requires much less programmer effort, although with less strict guarantees. A (pretty old) stream of work is to guarantee memory safety by using (usually a stack of) regions. Using region inference, a compiler can statically decide which region a piece of allocated data should go into, and deallocate the region when it goes out of scope.

Region inference is provably safe (can't deallocate reachable memory) and requires minimal programmer interference, but it is not "total" (i.e. it still can leak memory, although definitely much better than "do nothing"), so it's usually combined with GC in practice. The ~~MLton~~ ML Kit compiler uses regions to eliminate most GC calls, but it still has a GC because it would still leak memory otherwise. According to some of the early pioneers on regions, region inference wasn't actually invented for this purpose (it was for automatic parallelization, I think); but it just turned out it could be used for memory management as well.

For a starting point, I would say go for the paper "Implementation of the Typed Call-by-Value λ-calculus using a Stack of Regions" by Mads Tofte and Jean-Pierre Talpin. For more papers on region inference, look for other papers by M. Tofte and J.-P. Talpin, some of Pierre Jouvelot's work, as well as Greg Morrisett, Mike Hicks, and Dan Grossman's series of papers on Cyclone.


---

### Answer by username_4 on 2018-01-22. Score: -2

A trivial scheme for the "bare metal" systems is to simply disallow all runtime memory allocations. Remember, even the C `malloc/free` pair requires a runtime library. But even when all objects are defined at compile time, they can be defined in a typesafe way.

The chief problem here is the fiction of immutable values in pure functional languages, which are created while the program runs. Real hardware (and certainly bare metal systems) rely on mutable RAM, which is in limited supply. The runtime of a functional language implementation in practice dynamically allocates RAM as new "immutable" values are created, and garbage collects them when the "immutable" value is no longer needed.

And for most interesting problems, the lifetime of at least some values depends on runtime (user) input, so lifetimes can't be statically determined. But even if the lifetime doesn't depend on input, it can be highly non-trivial. Take the simple program repeatedly finding primes simply by checking every number in order, checking against all primes up to `sqrt(N)`. Clearly this needs keeps the primes and can recycle the memory used for the non-primes.


---

