My ambitious goal, with others, is to bring rigorous, scientific method to the specification of modern software systems, in line with standard engineering practice. My research advocates for formal software specifications that are: validated, with proper evidence that they describe what they should; useful, identifying compositional building blocks that enable scalable client reasoning; and just right, in that implementation details should not leak into the specification statement and the specification should be at the same level of abstraction as the client. This talk describes some of my work on the specification of languages, libraries and programs, determining what it means for a specification to be appropriate for the task at hand, properly evaluated and useful for real-world applications. In particular, I will describe my work on WasmCert, a mechanised specification of the WebAssembly language in the Coq and Isabelle theorem provers, and Gillian, a multi-language platform for compositional testing, specification and verification of programs, instantiated to the real-world languages JavaScript and C. I will place this research in the wider context of projects funded by the Research Institute on Verified Trustworthy Software Systems (VeTSS) in particular, and current international research in general.