Formally Specifying UIs (2018)

I recently read through “Designing the user interface with statecharts” by Horrocks. The arguments for are quite compelling, not just in terms of specifying, but also in terms of “designing”.<p>One illuminating example was a calculator application which had numerous errors and crashes which stemmed from intricacies of the UI implementation. By designing it as a statechart transitions are made visible and relationships are clear. The book provides three more examples.<p>In addition to the posted blog post, there are two more concepts in statecharts that I think are important: history and concurrency. They are not easy to explain in this comment, but the gist is that “history” allows for a simpler expression of returning to a previous state and “concurrency” formalizes the behavior of having concurrent states.<p>I’d recommend anyone to take a look at the book and I’d especially recommended to anyone who is a little skeptical of the idea of statecharts. I think the biggest argument against statecharts is that it requires you to specify your actual design, instead of just hacking on the code.

I am not a big fan of pseudo code unless:<p>1. You are designing a system that is handed off to an unrelated development team (common in agency work).<p>2. You need a stronger document of record because you lack enough trust in the development that a project plan plus design deliverables are insufficient when it comes to delivery and product quality.<p>When you go as deep as explicit pseudo code you are essentially building the project twice aside from testing and refactoring for edge cases. That is slow and expensive. If the UI is built using a very deep level of abstraction with lots of scaffolding I can see why the scope creep doesn&#x27;t matter, because extreme abstraction can easily blow out a project from 2 weeks to four months so why not add an addition 2 months for planning and review.<p>On the other hand UIs can be formally specified by code if the code when the code is small (not a super deep abstraction) and when the content&#x2F;behavior are separately defined from the code that builds the UI. Keep it simple and deliver more by intelligently doing less.

Thinking of interfaces as state machines can be valuable.<p>An area that I think about a lot is how effective are companies at spreading useful information to the people who can best utilize that information. Internal tools are interfaces to information. Wikis, mailing lists, code repositories, Q&amp;A boards, chat rooms are all different interfaces that I commonly search through for useful bits. A formal spec would help us quantify how effective our company is at spreading information. What information is commonly rewritten, what pages are hard to get to, which internal tool does a page of documentation belong to, etc.

I&#x27;m a fan of formal methods in general, but I&#x27;m not sure they&#x27;re a good fit for UI specification. Building user interfaces is all about flexibility—you need to be able to change the UI as you discover what works and what doesn&#x27;t. A rigid, pre-specified UI is almost always a bad UI.

One interesting thing about the various elm-like React reducer patterns&#x2F;libraries is that you essentially end up writing a state machine anyway. ReasonML&#x27;s react bindings have a reducer component available out of the box, making it easy to write a &#x27;pure&#x27; state machine and then wire it up to the UI via a React shell.<p>This allows you to do interesting things like generating instances of your UI state that match particular logical constraints (<a href="https:&#x2F;&#x2F;medium.com&#x2F;imandra&#x2F;constraint-solving-your-uis-8933f4cf8927" rel="nofollow">https:&#x2F;&#x2F;medium.com&#x2F;imandra&#x2F;constraint-solving-your-uis-8933f...</a>) or formally proving properties about the state machine (<a href="https:&#x2F;&#x2F;medium.com&#x2F;imandra&#x2F;verifying-reasonreact-component-logic-reasonml-imandra-e350d4812a9f" rel="nofollow">https:&#x2F;&#x2F;medium.com&#x2F;imandra&#x2F;verifying-reasonreact-component-l...</a>), but working directly with the code of the state machine itself rather than on a separate spec.<p>Disclaimer: I work for AI developing Imandra working on these tools.

I don&#x27;t know, this doesn&#x27;t make much sense to me. Usually you go from a set of specifications provided by a business analyst and then presuming you have a style guide and a &#x27;widget library&#x27;, the UX designer then &#x27;formally&#x27; implements a prototype which can then be tested asap, tweaked ad-nauseam.<p>Once that&#x27;s done, there goes your formal specification. We know what we&#x27;re doing, how we&#x27;re going to do it and we can work on the impl.

Creator of Sketch.systems Kevin Lynagh was interviewed in Future of Coding podcast while ago: <a href="https:&#x2F;&#x2F;futureofcoding.org&#x2F;episodes&#x2F;025.html" rel="nofollow">https:&#x2F;&#x2F;futureofcoding.org&#x2F;episodes&#x2F;025.html</a><p>Great podcast overall.

A random idea. Yesterday I opened The Gyllenhaal Experimet article on HN and noticed the chart that displays the tree of options and the number of people who took each path. It&#x27;s the first chart here:<p><a href="https:&#x2F;&#x2F;pudding.cool&#x2F;2019&#x2F;02&#x2F;gyllenhaal&#x2F;" rel="nofollow">https:&#x2F;&#x2F;pudding.cool&#x2F;2019&#x2F;02&#x2F;gyllenhaal&#x2F;</a><p>(Does anyone know what this type of chart is called?)<p>In relation to this article, it could be useful to watch how many people take paths across the states. Tracking that doesn&#x27;t necessitate a formal specification, but it helps. Then you could optimize common paths or eliminate unused states or transitions.

The look and feel of a UI is what is basically called a &quot;non-functional&quot; requirement. Altough this approach seems really helpful in specifying the app flow i think the small details which customers pay for, cannot be represented with this approach. Additionally, most customers I worked for might not understand these charts. Personally, I think tools like screenshots, click dummys or wireframes are more successful when specifying UIs for a customer. As a specification for a web designer it is helpful for sure...

Is it just me or did the mention of nesting FSMs immediately raise red flags? All I could think of was the rigid hierarchy problem found in OOP- what if your transitions don’t neatly fit in hierarchies? Everything still gets complex.<p>That said, if HSCs aren’t the solution, what is- specifically to the authors problem of having overly many transitions to ‘home’ states?

Tangential but the good looking page and dot-rendered gv don&#x27;t quite go together. Is there any &quot;beautiful&quot; and cleaner by default gv rendering engine (I know &#x27;cleanness&#x27; is an intractable problem for large graphs but this is a very small one)<p>What I&#x27;d like by default:<p>1) Borders and margins<p>2) Better colors<p>3) Decent font

Just thinking, I bet you could have a top level component (in React say) implement a state chart. Then the spec is the code, which is always nice. You might want parameterised states though (i.e. list into detail view) I wonder if that&#x27;s a thing.

A bit of a sidenote but FSM for UI is a reason why algebraic data types systems like swift with its powerful enum is so valuable.

Wow, I&#x27;m actually working on something that is eerily similar to this. Worried about competitors, haha, but glad to see that other people in the industry are leaning in the same direction.<p>He&#x27;s 100% right to conceive of interfaces as a finite state machine.

+1 for including sources for all graphs. Great for accessibility. Images are not enough for some people, and it&#x27;s nice you recognize that.

This is a great article. I wish the author had mentioned the outsize importance of pleasantness to UI however. An absolutely terrible unusable UI can still be formally correct.

Oh I see, Formal Methods are what we now call &#x27;planning ahead&#x27; now that Agile has made planning ahead unfashionable.