Semantic interfaces
      
        Graphical applications tend to focus on concrete representations of
        their user interfaces, restricting accessibility, extensibility, and
        interoperability, while GUI toolkits make even that rather hard to do
        well (see "Cross-platform GUI Toolkit Trainwreck", "Gui development is
        broken", as well as GTK, Pongo, xlib, Xft, FreeType, HarfBuzz,
        "State of Text Rendering (2012)").
        Some people stick to unixy tools, which reduce everything to text
        streams, but it's still much better in those aspects; others abuse web
        technologies or Emacs, which allow for different kinds of compromises;
        yet others experiment with semantic and/or declarative interfaces, about
        which this note is.
      
    
      Approaches
      
        The general approach is to describe both input and output in a way that
        leaves some freedom to implementations – that is, focusing on semantics,
        or on the model, possibly providing some hints for concrete interfaces.
        Examples of those, as well as of related or potentially useful for it
        technologies, are below.
      
      
        - HTML
 
        - 
          While it's a rather bad example in how it is used in practice, and
          rather restrictive by design, HTML tries to rely on semantic markup,
          can be accompanied by RDFa, and CSS can be seen as a representation
          recommendation. And it's the most widely used one.
        
 
        - XMPP Data Forms
 
        - XForms
 
        - Form descriptions targeting thin clients.
 
        - Fresnel
 
        - 
          An RDF display vocabulary, which provides hints on how to present
          RDF data.
        
 
        - Semantic forms
 
        - RDF-based form generators.
 
        - Plain RDF
 
        - Other combinations of XML, XSLT, RDF, CSS
 
        - 
          Generic RDF browsers and editors can be used as well, XML with
          associated XSLT can suggest representations.
        
 
        - SCXML
 
        - 
          A generic FSM description language, apparently intended for voice
          interfaces. Seems handy, though those can be embedded into
          types/propositions as well (e.g., Idris ST).
        
 
        - Declarative GUI libraries
 
        - 
          There is a variety of libraries that try to achieve usable declarative
          GUIs. A recent paper on the topic is Declarative GUIs: Simple,
          Consistent, and Verified, which also focuses on state machines and
          relies on dependent types, and there's more in the "Related Work"
          section. Being libraries, usually they are language-dependent, but
          they still seem nicer than more common approaches. Common GUI
          libraries, such as GTK, also support XML-based UI definitions
          (e.g., GtkBuilder).
        
 
        - swagger2 with Swagger UI (and perhaps servant-swagger)
 
        - Coalpit
 
        - Python Fire
 
        - 
          Haskell (and Python; didn't check it, but looks similar) packages
          generating interfaces out of types: JSON with OpenAPI in case of
          Swagger, command-line options and DSV with usage strings in case of
          Coalpit. These allow to easily expose complex structures (and
          functions operating on those) to other programs and users, and can
          potentially be extended to use RDF, presentation hints, and so on, and
          would get considerably more descriptive with dependent types.
        
 
        - My toy/prototype project
 
        - 
          Doesn't even have a proper name, but still serves as an example:
          semantic and textual UI descriptions are read as input and rendered,
          user actions produce output.
        
 
        - DBMS interfaces
 
        - 
          While most of the web applications seem to be little more than
          eye-candy and restrictive interfaces to databases, and there are
          generic interfaces to those, perhaps this is worth mentioning. Those
          are primarily about storage and retrieval, but business logic can be
          implemented in a DBMS as well.
        
 
        - Sequent calculus
 
        - Other proof calculi
 
        - 
          A handy way to deal with propositions in general, and may be useful
          for zooming user interfaces.
        
 
      
      
        The mentioned projects can be grouped into those focusing on fuzzy
        description logic, on intuitionistic logic, and the less generic,
        extensible, and/or semantic ones, which don't focus on a formal logic.
        Unsurprisingly, propositions are helpful to carry semantics.
      
    
      An interface outline
      
        Aiming exchange of propositions in different kinds of logic, perhaps UI
        should mostly deal with sequent calculus, while the program it
        communicates with would handle inference rules, read user-composed
        sequents, compose new ones. A loose analogy can be made with sequent
        calculus corresponding to a terminal, logic – to a shell, program – to
        streams of propositions (though probably in most cases it would be more
        handy to define custom inference rules in a program itself, perhaps
        plugging some kind of logic as a library), escape sequences – to
        rendering hints.
      
      
        There are nice opportunities for UI zomming with sequent
        calculus or other proof calculi, and the system may be rather
        simple/minimal and generic with it. But a bit of
        experimentation is needed to see how usable it would be, and
        it may be just a fun thing to play with.