We present the design of a typed assembly language with a property we dub \emph{total correctness}: well-typed programs are guaranteed to return their specified values.

The design combines a high-level specification language with a low level executable langauge of instructions and blocks, connecting the two together in a single assembly language by means of typing rules.

Our language is total (i.e. every program terminates), but expressive, with support for higher-order functions and control flow that goes beyond primitive recursion.

The design is currently at an early stage, but we plan to extend it to support more sophisticated type systems, as well as effects and other features needed in a practical system.