In this talk, I would like to present applications of maximal multi-focusing to programming languages problems -- in the simply-typed lambda-calculus with both negative types (such has functions) and positive types (such as sums). Focusing seems to be a key ingredient in extending existing intuitions on beta-eta equivalence from the purely negative fragment (functions and pairs) to a more diverse system with types of both polarities. I will present focusing and multi-focusing (for propositional intuitionistic logic, that is the simply-typed lambda-calculus), and its use to enumerate canonical inhabitants of a type (in particular testing whether a type has a unique inhabitant) and to test typed program equivalence (even in presence of the empty type).