The set theory "New Foundations" or NF introduced by W.V.O. Quine in 1935 is
discussed, along with related systems. It is argued that, in spite of the fact that the consistency of NF
remains an open question, the relative consistency results for NFU obtained by R. B. Jensen in 1969
demonstrate that Quine's general approach can be used successfully. The development of basic
mathematical concepts in a version of NFU is outlined. The interpretation of set theories of the usual
type in extensions of NFU is discussed. The problems with NF itself are discussed, and other
fragments of NF known to be consistent are briefly introduced. The relative merits of Quine-style and
Zermelo-style set theories are considered from a philosophical standpoint. Finally, systems of untyped
combinatory logic or $\lambda$-calculus related to NF and its fragments are introduced, and their relation to
an abstract model of programming is outlined.