Computer Science Thesis Oral

Friday, May 8, 2020 - 1:30pm to 3:30pm

Location:

Virtual Presentation Remote Access Enabled - Zoom

Speaker:

MICHAEL J. COBLENZ, Ph.D. Student https://www.cs.cmu.edu/~mcoblenz/

User-Centered Design of Principled Programming Languages

Programming languages exist to enable people to create and maintain software as effectively as possible. They are subject to two very different sets of requirements: first, the need to provide strong safety guarantees to protect against bugs; and second, the need for users to effectively and efficiently write software that meets their functional and quality requirements. This thesis argues that fusing formal methods for reasoning about programming languages with user-centered design methods is a practical approach to designing languages that make programmers more effective.

The hypothesis is supported by two language design projects, which integrate a variety of human-centered approaches into the programming language design process. Glacier is an extension to Java that enforces transitive class immutability, which is a much stronger property than that provided by languages that are in use today. I motivated the design of Glacier by interviewing professional software engineers. I compared Glacier to to Java’s final keyword in a lab study, finding both that Glacier is more effective at expressing immutability than final and that Glacier detects bugs that users are likely to insert in code.

I also developed Obsidian, a new programming language for blockchain application development, where correctness is particularly important. Motivated by observations of blockchain applications, Obsidian uses typestate, which lifts dynamic state into static types, to provide static guarantees regarding object state. Obsidian also supports resources via linear types, which ensure that owning references to resources are not accidentally lost.

Typical typestate systems have a complex set of permissions that provides safety properties, but these systems focused on expressiveness rather than on usability. In order to make Obsidian as usable as possible, I based its design on the results of formative studies with programmers. I evaluated Obsidian with two case studies and a summative user study, showing that Obsidian can be used to implement relevant programs; that programmers who use Solidity, a popular language for writing smart contracts, accidentally insert bugs that Obsidian rules out; and that most of the participants could learn Obsidian and complete programming tasks after only a short training period.

Thesis Committee:
Jonathan Aldrich (Co-Chair)
Brad A. Myers (Co-Chair)
Frank Pfenning
Joshua Sunshine
Gail Murphy (University of British Columbia)

Zoom Participation Enabled. See announcement.

For More Information, Contact:

Keywords:

Thesis Oral