Type-based memory safety without manual memory manage or runtime garbage collection? 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?
Roughly speaking, there are two main strategies for safe manual memory management. 


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. As an aside, the LFPL calculus Damiano Mazza mentioned is also linear,  has a full language derived from it in the RAML language. 

If you are interested in Idris-style verification, you should look at Xi et al's ATS language, 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 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 (or even my own  Integrating Linear and Dependent Types), 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, which is a substructural logic related to linear logic that has seen great success as the assertion language for Hoare logics for pointer programs.
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 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 at Princeton and the 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.