Verification tools like Dafny are slowly being adopted in software engineering practice — if not for entire projects, then at least for safety or security critical kernels of large systems. Verification offers a direct to the essential complexity of software development – building a correct system — rather than the accidental complexity induced by learning how to use a particular language or toolset, with their accompanying quirks, oddities, and idiosyncrasies.

Graduate software engineers need to be exposed to verification tools, and the formal methods, techniques, and concepts underlying those tools, even if only to be prepared when they come across those tools later in their professional careers. Unfortunately, we have found that many software engineering students resist formal methods — whether due to perceived difficulty, suspected practical irrelevance, or overall mathematicity.

In this presentation, we will outline how Dafny can be incorporated into a programming first software correctness course. We then reflect on some particular features of Dafny’s design, and hypothesize how relatively small improvements to Dafny could remove some of the accidental complexity which seems attendant with students learning the language, hopefully allowing them to focus further on the essential complexity of verification.

James Noble (kjx@acm.org) is an independent creative researcher & programmer based in Wellington, New Zealand. After completing honours and doctoral degrees at Victoria University of Wellington (VUW), James worked at the University of Technology, Sydney, the Microsoft Research Institute at Macquarie University, and is recovering from a long stint as professor of computer science & software engineering at VUW.

James’s research centres around software design. This includes the design of the users’ interface, the parts of software that users have to deal with every day, and the programmers’ interface, the internal structures and organisations of software that programmers see only when they are designing, building, or modifying software.

James’s research in both of these areas is coloured by a longstanding interest in object-oriented approaches to design, and topics he has studied range from aliasing and object ownership, programming languages, design patterns, agile methodology, via usability, visualisation and computer music, to postmodernism and the semiotics of programming.