The open sets of a topology space have a nice algebraic structure, and it turns out that much of classical topology can be formulated in terms of this structure without reference to any underlying set of points. Like many such algebraic lattice structures, we can regard it as a system of propositions in logic with meet (intersection) and join (union) in the lattice corresponding to logical "and" and to logical "or". From this perspective, a topological space is a propositional theory with models of the theory given by the points of the space. With suitable separation properties, the models are entirely determined by the open sets. In many familiar cases, we can give the lattice of opens first and then derive the points from this. In general however, such a lattice might have no points at all. In logical terms, some propositional theories can be consistent but still fail to have any set-based models. Such generalized lattices of opens are often called locales, and the corresponding theories are those of geometric propositional logic. In this talk, we'll consider the fundamental relationship between locales and traditional topology, discuss why one might be interested in point-free topology, and consider examples of consistent theories which fail to have models in the usual sense.