  We propose here to look at how abstract a model of a usable system can be,
but still say something useful and interesting, so this paper is an exercise in
abstraction and formalisation, with usability-of-design as an example target
use.
  We take the view that when we claim to be designing a usable system we have,
at the very least, to give assurances about its usability properties. This is a
very abstract notion, but provides the basis for future work, and shows, even
at this level that there are things to say about the (very concrete) business
of designing and building usable, interactive systems.
  Various forms of verification and validation can provide a high level of
assurance but it can be very costly, and there is clearly a lot of resistance
to doing things this way.
  In this paper, we introduce the idea of usable-by-construction, which adopts
and applies the ideas of correct-by-construction to (very abstractly) thinking
about usable systems.
  We give a set of construction rules or tactics to develop designs of usable
systems, and we also formalize them into a state suitable for, for example, a
proof assistant to check claims made for the system as designed.
  In the future, these tactics would allow us to create systems that have the
required usability properties and thus provide a basis to a
usable-by-construction system. Also, we should then go on to show that the
tactics preserve properties by using an example system with industrial strength
requirements. And we might also consider future research directions.
