== Goal A memory-safe language with a simple translator to x86 that can be feasibly written in x86. == Definitions of terms Memory-safe: it should be impossible to: a) create a pointer out of arbitrary data, or b) to access heap memory after it's been freed. Simple: do all the work in a 2-pass translator: Pass 1: check each instruction's types in isolation. Pass 2: emit code for each instruction in isolation. == types int char (address _ t), t ∋ {stack, heap, global} (array _ t), t ∋ {stack, heap, global} stack addresses can't be copied to heap or global heap addresses can't be copied [1] global addresses you're free to use anywhere [1] (address _ heap) can't be copied or stored, can't be part of a type or choice. Only thing you can do with it is access it from the register you wrote it to. And even that not past a call instruction. Important detail: `free()` is a call. So an address to something on the heap can never be invalid if the program type-checks. : (address T m) <- advance : (array T m), : (index T)