George Spencer-Brown's »Laws of Form« (LoF) provided an important formalism and important insights for all kinds of fields in 1969. He made it possible to calculate with layered, self-referential spaces, time, and even the »blank« space using the distinction as a basal operation. However, with a few exceptions in sociology (Niklas Luhmann & Dirk Baecker) and mathematics (Louis H. Kauffman), cybernetic biology (Humberto Maturana & Francisco varela) the work has found few practical use cases. User interfaces, on the other hand, be they graphical or e.g. conversational, are practically designed, described and most importantly used every day - they are the experiential interfaces of our (digital) environments. Although some formalisms for these have been developed in recent years, they are on the one hand very domain-specific and on the other hand do not allow to calculate with the interfaces and thus our (digital) environments. It turns out that, in the spirit of LoF, the fundamental operation for user interfaces is also the distinction. In this paper, a formalism for user interfaces based on LoF shall be worked out, which allows to describe, compute and (domain-spanning) transform them solely by means of the distinction. In particular, it will be shown that this is an exceedingly natural way to describe and reason about (self-referential) graphical user interfaces (which can be thought of as distinctive layered spaces) and to find fundamental connections between them and other disciplines. This work will maybe lay the foundation for future designers to later develop automatic theorem provers for interfaces and to perform formal verifications.