Chapter 16: Verified Memory Management

We survey some works on approaches to statically verifying programs with explicit memory management. My question is, can we have a pure functional programming language with explicit memory management, using only rather light annotations to show the compiler that memory is being used correctly? How close is Rust to this goal? This chapter only scratches the surface of the research in this area, neglecting (sadly) many important works.