We will talk about TLA. About the logic, its uses, its model theory, and the possibilities for mechanization in Nuprl.