Due to Paul Taylor, Abstract Stone Duality (ASD) is a reaxiomatisation of the notions of space and map in general topology in terms of a λ-calculus of computable continuous functions and predicates that is both constructive and computable.
The topology on a space is treated not as a discrete lattice, but as an exponential object of the same category as the original space, with an associated λ-calculus (which includes an internal lattice structure). Every expression in the λ-calculus denotes both a continuous function and a program. ASD does not use the category of sets (or any topos), but the full subcategory of overt discrete objects plays this role (an overt object is the dual to a compact object), forming an arithmetic universe (a pretopos with lists) with general recursion; an optional ‘underlying set’ axiom (which is not predicative) will make this a topos.
The classical (but not constructive) theory of locally compact sober topological spaces is a model of ASD, as is the theory of locally compact locales over any topos (even constructively). Taylor has recently removed the restriction of local compactness.