This chapter explores the metalanguage, ML, and its relationship to the object language, Nuprl . It examines details of the interface and explains how ML allows extensions to the deductive apparatus. Beginning with a brief summary of ML as a general purpose language, the chapter presents a detailed look at tactics , which are functions for developing proofs, and describes tools for writing tactics and ways to combine tactics. The chapter concludes with some example tactics.