Ursula Martin

This paper presents the collaborative European ESPRIT ProCoS projects on “Provably Correct Systems”, and associated initiatives of the 1990s. The influence of the projects in the field of formal methods is also discussed. A general overview of the projects is provided, together with a number of reminiscences by those involved with the projects, including the influence on the subsequent careers of participants. The projects addressed the issues of connecting formal approaches at different connected levels of formality, including requirements, specification, and compilation down to machine code and even directly into hardware. The investigations were based on a representative subset of the programming language Occam, which was subsequently extended by elements indicative of particular problems of compilation, yet not found in Occam, and the related Transputer microprocessor. In practice, two of the most important and enduring results after the projects were Duration Calculus and Unifying Theories of Programming, both subfields of formal methods, with associated communities of researchers and practitioners.

Records of online collaborative mathematical activity provide us with a novel, rich, searchable, accessible and sizeable source of data for empirical investigations into mathematical practice. In this paper we discuss how the resources of crowdsourced mathematics can be used to help formulate and answer questions about mathematical practice, and what their limitations might be. We describe quantitative approaches to studying crowdsourced mathematics, reviewing work from cognitive history (comparing individual and collaborative proofs); social psychology (on the prospects for a measure of collective intelligence); human–computer interaction (on the factors that led to the success of one such project); network analysis (on the differences between collaborations on open research problems and known-but-hard problems); and argumentation theory (on modelling the argument structures of online collaborations). We also give an overview of qualitative approaches, reviewing work from empirical philosophy (on explanation in crowdsourced mathematics); sociology of scientific knowledge (on conventions and conversations in online mathematics); and ethnography (on contrasting conceptions of collaboration). We suggest how these diverse methods can be applied to crowdsourced mathematics and when each might be appropriate.

This empirical study explored how research can generate impacts by investigating different sorts of impacts from one academic field—mathematics—and the diverse mechanisms generating them. The multi-method study triangulated across: (1 and 2) content analysis of impact case studies and environment descriptions submitted to the UK Research Excellence Framework (REF) assessment; (3 and 4) a survey and focus group of heads of mathematics departments; and (5) semi-structured interviews. Mathematics has had a full range of impact types, particularly conceptual impacts, although more tangible instrumental impacts were prioritized for REF. Multiple mechanisms were utilized, but seldom appeared in REF case studies. Long-term relationship building and interdisciplinarity are particularly important. Departmental culture and certain knowledge intermediaries can play proactive roles. In sharp contrast to simplistic linear narratives, we suggest that appreciation of diverse impact types, multiple, often informal, mechanisms and dynamic environments will enhance the likelihood of meaningful impacts being generated.

Professor Ursula Martin of the Department of Computer Science at the University of Oxford celebrates the 200th anniversary of the birth of Ada Lovelace with a look at her life and legacy.

For centuries, the highest level of mathematics has been seen as an isolated creative activity, to produce a proof for review and acceptance by research peers. Mathematics is now at a remarkable inflexion point, with new technology radically extending the power and limits of individuals. ‘Crowdsourcing’ pulls together diverse experts to solve problems; symbolic computation tackles huge routine calculations; and computers, using programs designed to verify hardware, check proofs that are just too long and complicated for any human to comprehend. ‘Social machines’ are new paradigm, identified by Berners-Lee, for viewing a combination of people and computers as a single problem-solving entity. This paper outlines a research agenda for a new vision of a mathematics social machine, a combination of people, computers, and archives to create and apply mathematics, and places it in the context of verification research, computational logic and Roy Dyckhoff's pioneering work on computer proof.

Real number theorem proving has many uses, particularly for verification of safety critical systems and systems for which design errors may be costly. We discuss a chain of developments building on real number theorem proving in PVS. This leads from the verification of aspects of an air traffic control system, through work on the integration of computer algebra and automated theorem proving to a new tool, NRV, first presented here that builds on the capabilities of Maple and PVS to provide a verified and automatic analysis of Nichols plots. This automates a standard technique used by control engineers and greatly improves assurance compared with the traditional method of visual inspection of the Nichols plots.