-
Profiling Programming Language Learning
Authors:
Will Crichton,
Shriram Krishnamurthi
Abstract:
This paper documents a year-long experiment to "profile" the process of learning a programming language: gathering data to understand what makes a language hard to learn, and using that data to improve the learning process. We added interactive quizzes to The Rust Programming Language, the official textbook for learning Rust. Over 13 months, 62,526 readers answered questions 1,140,202 times. First…
▽ More
This paper documents a year-long experiment to "profile" the process of learning a programming language: gathering data to understand what makes a language hard to learn, and using that data to improve the learning process. We added interactive quizzes to The Rust Programming Language, the official textbook for learning Rust. Over 13 months, 62,526 readers answered questions 1,140,202 times. First, we analyze the trajectories of readers. We find that many readers drop-out of the book early when faced with difficult language concepts like Rust's ownership types. Second, we use classical test theory and item response theory to analyze the characteristics of quiz questions. We find that better questions are more conceptual in nature, such as asking why a program does not compile vs. whether a program compiles. Third, we performed 12 interventions into the book to help readers with difficult questions. We find that on average, interventions improved quiz scores on the targeted questions by +20%. Fourth, we show that our technique can likely generalize to languages with smaller user bases by simulating our statistical inferences on small N. These results demonstrate that quizzes are a simple and useful technique for understanding language learning at all scales.
△ Less
Submitted 2 January, 2024;
originally announced January 2024.
-
A Core Calculus for Documents
Authors:
Will Crichton,
Shriram Krishnamurthi
Abstract:
Passive documents and active programs now widely comingle. Document languages include Turing-complete programming elements, and programming languages include sophisticated document notations. However, there are no formal foundations that model these languages. This matters because the interaction between document and program can be subtle and error-prone. In this paper we describe several such pro…
▽ More
Passive documents and active programs now widely comingle. Document languages include Turing-complete programming elements, and programming languages include sophisticated document notations. However, there are no formal foundations that model these languages. This matters because the interaction between document and program can be subtle and error-prone. In this paper we describe several such problems, then taxonomize and formalize document languages as levels of a document calculus. We employ the calculus as a foundation for implementing complex features such as reactivity, as well as for proving theorems about the boundary of content and computation. We intend for the document calculus to provide a theoretical basis for new document languages, and to assist designers in cleaning up the unsavory corners of existing languages.
△ Less
Submitted 14 November, 2023; v1 submitted 6 October, 2023;
originally announced October 2023.
-
Debugging Trait Errors as Logic Programs
Authors:
Gavin Gray,
Will Crichton
Abstract:
Rust uses traits to define units of shared behavior. Trait constraints build up an implicit set of first-order hereditary Harrop clauses which is executed by a powerful logic programming engine in the trait system. But that power comes at a cost: the number of traits in Rust libraries is increasing, which puts a growing burden on the trait system to help programmers diagnose errors. Beyond a certa…
▽ More
Rust uses traits to define units of shared behavior. Trait constraints build up an implicit set of first-order hereditary Harrop clauses which is executed by a powerful logic programming engine in the trait system. But that power comes at a cost: the number of traits in Rust libraries is increasing, which puts a growing burden on the trait system to help programmers diagnose errors. Beyond a certain size of trait constraints, compiler diagnostics fall off the edge of a complexity cliff, leading to useless error messages. Crate maintainers have created ad-hoc solutions to diagnose common domain-specific errors, but the problem of diagnosing trait errors in general is still open. We propose a trait debugger as a means of getting developers the information necessary to diagnose trait errors in any domain and at any scale. Our proposed tool will extract proof trees from the trait solver, and it will interactively visualize these proof trees to facilitate debugging of trait errors.
△ Less
Submitted 10 September, 2023;
originally announced September 2023.
-
A Grounded Conceptual Model for Ownership Types in Rust
Authors:
Will Crichton,
Gavin Gray,
Shriram Krishnamurthi
Abstract:
Programmers learning Rust struggle to understand ownership types, Rust's core mechanism for ensuring memory safety without garbage collection. This paper describes our attempt to systematically design a pedagogy for ownership types. First, we studied Rust developers' misconceptions of ownership to create the Ownership Inventory, a new instrument for measuring a person's knowledge of ownership. We…
▽ More
Programmers learning Rust struggle to understand ownership types, Rust's core mechanism for ensuring memory safety without garbage collection. This paper describes our attempt to systematically design a pedagogy for ownership types. First, we studied Rust developers' misconceptions of ownership to create the Ownership Inventory, a new instrument for measuring a person's knowledge of ownership. We found that Rust learners could not connect Rust's static and dynamic semantics, such as determining why an ill-typed program would (or would not) exhibit undefined behavior. Second, we created a conceptual model of Rust's semantics that explains borrow checking in terms of flow-sensitive permissions on paths into memory. Third, we implemented a Rust compiler plugin that visualizes programs under the model. Fourth, we integrated the permissions model and visualizations into a broader pedagogy of ownership by writing a new ownership chapter for The Rust Programming Language, a popular Rust textbook. Fifth, we evaluated an initial deployment of our pedagogy against the original version, using reader responses to the Ownership Inventory as a point of comparison. Thus far, the new pedagogy has improved learner scores on the Ownership Inventory by an average of 9% ($N = 342, d = 0.56$).
△ Less
Submitted 8 September, 2023;
originally announced September 2023.
-
Typed Design Patterns for the Functional Era
Authors:
Will Crichton
Abstract:
This paper explores how design patterns could be revisited in the era of mainstream functional programming languages. I discuss the kinds of knowledge that ought to be represented as functional design patterns: architectural concepts that are relatively self-contained, but whose entirety cannot be represented as a language-level abstraction. I present four concrete examples embodying this idea: th…
▽ More
This paper explores how design patterns could be revisited in the era of mainstream functional programming languages. I discuss the kinds of knowledge that ought to be represented as functional design patterns: architectural concepts that are relatively self-contained, but whose entirety cannot be represented as a language-level abstraction. I present four concrete examples embodying this idea: the Witness, the State Machine, the Parallel Lists, and the Registry. Each pattern is implemented in Rust to demonstrate how careful use of a sophisticated type system can better model each domain construct and thereby catch user mistakes at compile-time.
△ Less
Submitted 13 July, 2023;
originally announced July 2023.
-
Modular Information Flow through Ownership
Authors:
Will Crichton,
Marco Patrignani,
Maneesh Agrawala,
Pat Hanrahan
Abstract:
Statically analyzing information flow, or how data influences other data within a program, is a challenging task in imperative languages. Analyzing pointers and mutations requires access to a program's complete source. However, programs often use pre-compiled dependencies where only type signatures are available. We demonstrate that ownership types can be used to soundly and precisely analyze info…
▽ More
Statically analyzing information flow, or how data influences other data within a program, is a challenging task in imperative languages. Analyzing pointers and mutations requires access to a program's complete source. However, programs often use pre-compiled dependencies where only type signatures are available. We demonstrate that ownership types can be used to soundly and precisely analyze information flow through function calls given only their type signature. From this insight, we built Flowistry, a system for analyzing information flow in Rust, an ownership-based language. We prove the system's soundness as a form of noninterference using the Oxide formal model of Rust. Then we empirically evaluate the precision of Flowistry, showing that modular flows are identical to whole-program flows in 94% of cases drawn from large Rust codebases. We illustrate the applicability of Flowistry by using it to implement prototypes of a program slicer and an information flow control system.
△ Less
Submitted 15 March, 2022; v1 submitted 26 November, 2021;
originally announced November 2021.
-
Automating Program Structure Classification
Authors:
Will Crichton,
Georgia Gabriela Sampaio,
Pat Hanrahan
Abstract:
When students write programs, their program structure provides insight into their learning process. However, analyzing program structure by hand is time-consuming, and teachers need better tools for computer-assisted exploration of student solutions. As a first step towards an education-oriented program analysis toolkit, we show how supervised machine learning methods can automatically classify st…
▽ More
When students write programs, their program structure provides insight into their learning process. However, analyzing program structure by hand is time-consuming, and teachers need better tools for computer-assisted exploration of student solutions. As a first step towards an education-oriented program analysis toolkit, we show how supervised machine learning methods can automatically classify student programs into a predetermined set of high-level structures. We evaluate two models on classifying student solutions to the Rainfall problem: a nearest-neighbors classifier using syntax tree edit distance and a recurrent neural network. We demonstrate that these models can achieve 91% classification accuracy when trained on 108 programs. We further explore the generality, trade-offs, and failure cases of each model.
△ Less
Submitted 15 January, 2021;
originally announced January 2021.
-
The Role of Working Memory in Program Tracing
Authors:
Will Crichton,
Maneesh Agrawala,
Pat Hanrahan
Abstract:
Program tracing, or mentally simulating a program on concrete inputs, is an important part of general program comprehension. Programs involve many kinds of virtual state that must be held in memory, such as variable/value pairs and a call stack. In this work, we examine the influence of short-term working memory (WM) on a person's ability to remember program state during tracing. We first confirm…
▽ More
Program tracing, or mentally simulating a program on concrete inputs, is an important part of general program comprehension. Programs involve many kinds of virtual state that must be held in memory, such as variable/value pairs and a call stack. In this work, we examine the influence of short-term working memory (WM) on a person's ability to remember program state during tracing. We first confirm that previous findings in cognitive psychology transfer to the programming domain: people can keep about 7 variable/value pairs in WM, and people will accidentally swap associations between variables due to WM load. We use a restricted focus viewing interface to further analyze the strategies people use to trace through programs, and the relationship of tracing strategy to WM. Given a straight-line program, we find half of our participants traced a program from the top-down line-by-line (linearly), and the other half start at the bottom and trace upward based on data dependencies (on-demand). Participants with an on-demand strategy made more WM errors while tracing straight-line code than with a linear strategy, but the two strategies contained an equal number of WM errors when tracing code with functions. We conclude with the implications of these findings for the design of programming tools: first, programs should be analyzed to identify and refactor human-memory-intensive sections of code. Second, programming environments should interactively visualize variable metadata to reduce WM load in accordance with a person's tracing strategy. Third, tools for program comprehension should enable externalizing program state while tracing.
△ Less
Submitted 15 January, 2021;
originally announced January 2021.
-
The Usability of Ownership
Authors:
Will Crichton
Abstract:
Ownership is the concept of tracking aliases and mutations to data, useful for both memory safety and system design. The Rust programming language implements ownership via the borrow checker, a static analyzer that extends the core type system. The borrow checker is a notorious learning barrier for new Rust users. In this paper, I focus on the gap between understanding ownership in theory versus i…
▽ More
Ownership is the concept of tracking aliases and mutations to data, useful for both memory safety and system design. The Rust programming language implements ownership via the borrow checker, a static analyzer that extends the core type system. The borrow checker is a notorious learning barrier for new Rust users. In this paper, I focus on the gap between understanding ownership in theory versus its implementation in the borrow checker. As a sound and incomplete analysis, compiler errors may arise from either ownership-unsound behavior or limitations of the analyzer. Understanding this distinction is essential for fixing ownership errors. But how are users actually supposed to make the correct inference? Drawing on my experience with using and teaching Rust, I explore the many challenges in interpreting and responding to ownership errors. I also suggest educational and automated interventions that could improve the usability of ownership.
△ Less
Submitted 22 September, 2021; v1 submitted 11 November, 2020;
originally announced November 2020.
-
Documentation Generation as Information Visualization
Authors:
Will Crichton
Abstract:
Automatic documentation generation tools, or auto docs, are widely used to visualize information about APIs. However, each auto doc tool comes with its own unique representation of API information. In this paper, I use an information visualization analysis of auto docs to generate potential design principles for improving their usability. Developers use auto docs as a reference by looking up relev…
▽ More
Automatic documentation generation tools, or auto docs, are widely used to visualize information about APIs. However, each auto doc tool comes with its own unique representation of API information. In this paper, I use an information visualization analysis of auto docs to generate potential design principles for improving their usability. Developers use auto docs as a reference by looking up relevant API primitives given partial information, or leads, about its name, type, or behavior. I discuss how auto docs can better support searching and scanning on these leads, e.g. by providing more information-dense visualizations of method signatures.
△ Less
Submitted 11 November, 2020;
originally announced November 2020.
-
Analyzing Who and What Appears in a Decade of US Cable TV News
Authors:
James Hong,
Will Crichton,
Haotian Zhang,
Daniel Y. Fu,
Jacob Ritchie,
Jeremy Barenholtz,
Ben Hannel,
Xinwei Yao,
Michaela Murray,
Geraldine Moriba,
Maneesh Agrawala,
Kayvon Fatahalian
Abstract:
Cable TV news reaches millions of U.S. households each day, meaning that decisions about who appears on the news and what stories get covered can profoundly influence public opinion and discourse. We analyze a data set of nearly 24/7 video, audio, and text captions from three U.S. cable TV networks (CNN, FOX, and MSNBC) from January 2010 to July 2019. Using machine learning tools, we detect faces…
▽ More
Cable TV news reaches millions of U.S. households each day, meaning that decisions about who appears on the news and what stories get covered can profoundly influence public opinion and discourse. We analyze a data set of nearly 24/7 video, audio, and text captions from three U.S. cable TV networks (CNN, FOX, and MSNBC) from January 2010 to July 2019. Using machine learning tools, we detect faces in 244,038 hours of video, label each face's presented gender, identify prominent public figures, and align text captions to audio. We use these labels to perform screen time and word frequency analyses. For example, we find that overall, much more screen time is given to male-presenting individuals than to female-presenting individuals (2.4x in 2010 and 1.9x in 2019). We present an interactive web-based tool, accessible at https://tvnews.stanford.edu, that allows the general public to perform their own analyses on the full cable TV news data set.
△ Less
Submitted 24 January, 2022; v1 submitted 13 August, 2020;
originally announced August 2020.
-
Rekall: Specifying Video Events using Compositions of Spatiotemporal Labels
Authors:
Daniel Y. Fu,
Will Crichton,
James Hong,
Xinwei Yao,
Haotian Zhang,
Anh Truong,
Avanika Narayan,
Maneesh Agrawala,
Christopher Ré,
Kayvon Fatahalian
Abstract:
Many real-world video analysis applications require the ability to identify domain-specific events in video, such as interviews and commercials in TV news broadcasts, or action sequences in film. Unfortunately, pre-trained models to detect all the events of interest in video may not exist, and training new models from scratch can be costly and labor-intensive. In this paper, we explore the utility…
▽ More
Many real-world video analysis applications require the ability to identify domain-specific events in video, such as interviews and commercials in TV news broadcasts, or action sequences in film. Unfortunately, pre-trained models to detect all the events of interest in video may not exist, and training new models from scratch can be costly and labor-intensive. In this paper, we explore the utility of specifying new events in video in a more traditional manner: by writing queries that compose outputs of existing, pre-trained models. To write these queries, we have developed Rekall, a library that exposes a data model and programming model for compositional video event specification. Rekall represents video annotations from different sources (object detectors, transcripts, etc.) as spatiotemporal labels associated with continuous volumes of spacetime in a video, and provides operators for composing labels into queries that model new video events. We demonstrate the use of Rekall in analyzing video from cable TV news broadcasts, films, static-camera vehicular video streams, and commercial autonomous vehicle logs. In these efforts, domain experts were able to quickly (in a few hours to a day) author queries that enabled the accurate detection of new events (on par with, and in some cases much more accurate than, learned approaches) and to rapidly retrieve video clips for human-in-the-loop tasks such as video content curation and training data curation. Finally, in a user study, novice users of Rekall were able to author queries to retrieve new events in video given just one hour of query development time.
△ Less
Submitted 7 October, 2019;
originally announced October 2019.
-
Human-Centric Program Synthesis
Authors:
Will Crichton
Abstract:
Program synthesis techniques offer significant new capabilities in searching for programs that satisfy high-level specifications. While synthesis has been thoroughly explored for input/output pair specifications (programming-by-example), this paper asks: what does program synthesis look like beyond examples? What actual issues in day-to-day development would stand to benefit the most from synthesi…
▽ More
Program synthesis techniques offer significant new capabilities in searching for programs that satisfy high-level specifications. While synthesis has been thoroughly explored for input/output pair specifications (programming-by-example), this paper asks: what does program synthesis look like beyond examples? What actual issues in day-to-day development would stand to benefit the most from synthesis? How can a human-centric perspective inform the exploration of alternative specification languages for synthesis? I sketch a human-centric vision for program synthesis where programmers explore and learn languages and APIs aided by a synthesis tool.
△ Less
Submitted 26 September, 2019;
originally announced September 2019.
-
From Theory to Systems: A Grounded Approach to Programming Language Education
Authors:
Will Crichton
Abstract:
I present a new approach to teaching a graduate-level programming languages course focused on using systems programming ideas and languages like WebAssembly and Rust to motivate PL theory. Drawing on students' prior experience with low-level languages, the course shows how type systems and PL theory are used to avoid tricky real-world errors that students encounter in practice. I reflect on the cu…
▽ More
I present a new approach to teaching a graduate-level programming languages course focused on using systems programming ideas and languages like WebAssembly and Rust to motivate PL theory. Drawing on students' prior experience with low-level languages, the course shows how type systems and PL theory are used to avoid tricky real-world errors that students encounter in practice. I reflect on the curricular design and lessons learned from two years of teaching at Stanford, showing that integrating systems ideas can provide students a more grounded and enjoyable education in programming languages. The curriculum, course notes, and assignments are freely available: http://cs242.stanford.edu/f18/
△ Less
Submitted 14 April, 2019;
originally announced April 2019.
-
Identifying Barriers to Adoption for Rust through Online Discourse
Authors:
Anna Zeng,
Will Crichton
Abstract:
Rust is a low-level programming language known for its unique approach to memory-safe systems programming and for its steep learning curve. To understand what makes Rust difficult to adopt, we surveyed the top Reddit and Hacker News posts and comments about Rust; from these online discussions, we identified three hypotheses about Rust's barriers to adoption. We found that certain key features, idi…
▽ More
Rust is a low-level programming language known for its unique approach to memory-safe systems programming and for its steep learning curve. To understand what makes Rust difficult to adopt, we surveyed the top Reddit and Hacker News posts and comments about Rust; from these online discussions, we identified three hypotheses about Rust's barriers to adoption. We found that certain key features, idioms, and integration patterns were not easily accessible to new users.
△ Less
Submitted 4 January, 2019;
originally announced January 2019.
-
Scanner: Efficient Video Analysis at Scale
Authors:
Alex Poms,
Will Crichton,
Pat Hanrahan,
Kayvon Fatahalian
Abstract:
A growing number of visual computing applications depend on the analysis of large video collections. The challenge is that scaling applications to operate on these datasets requires efficient systems for pixel data access and parallel processing across large numbers of machines. Few programmers have the capability to operate efficiently at these scales, limiting the field's ability to explore new…
▽ More
A growing number of visual computing applications depend on the analysis of large video collections. The challenge is that scaling applications to operate on these datasets requires efficient systems for pixel data access and parallel processing across large numbers of machines. Few programmers have the capability to operate efficiently at these scales, limiting the field's ability to explore new applications that leverage big video data. In response, we have created Scanner, a system for productive and efficient video analysis at scale. Scanner organizes video collections as tables in a data store optimized for sampling frames from compressed video, and executes pixel processing computations, expressed as dataflow graphs, on these frames. Scanner schedules video analysis applications expressed using these abstractions onto heterogeneous throughput computing hardware, such as multi-core CPUs, GPUs, and media processing ASICs, for high-throughput pixel processing. We demonstrate the productivity of Scanner by authoring a variety of video processing applications including the synthesis of stereo VR video streams from multi-camera rigs, markerless 3D human pose reconstruction from video, and data-mining big video datasets such as hundreds of feature-length films or over 70,000 hours of TV news. These applications achieve near-expert performance on a single machine and scale efficiently to hundreds of machines, enabling formerly long-running big video data analysis tasks to be carried out in minutes to hours.
△ Less
Submitted 18 May, 2018;
originally announced May 2018.
