Background: Proof Blocks is a software tool that enables students to construct proofs by assembling prewritten lines and gives them automated feedback. Prior work on learning gains from Proof Blocks has focused on comparing learning gains from Proof Blocks against other learning activities such as writing proofs or reading.

Background : Proof Blocks is a software tool that enables students to construct proofs by assembling prewritten lines and gives them automated feedback. Prior research has shown that students learn as much from an activity where they use Proof Blocks as where they write proofs. However, in both cases students first read a book chapter. Prior research was not able to differentiate between the learning gains achieved from reading versus proof practice. Purpose : This study aims to measure learning gains from reading a book chapter versus completing Proof Blocks. Methods : We conducted a randomized controlled trial with three experimental groups: one that only read a book chapter, one that only completed Proof Blocks, and one that did both. Findings : The group that completed only Proof Blocks had the smallest learning gains. The group that read the book chapter and completed the Proof Blocks activity performed marginally better than students who only read the book chapter, but it is not clear if the source of this improvement was the Proof Blocks or just exposure to more examples.

Proof Blocks is a software tool that provides students with a scaffolded proof-writing experience, allowing them to drag and drop prewritten proof lines into the correct order instead of starting from scratch. In this paper we describe a randomized controlled trial designed to measure the learning gains of using Proof Blocks for students learning proof by induction. The study participants were 332 students recruited after completing the first month of their discrete mathematics course. Students in the study took a pretest and read lecture notes on proof by induction, completed a brief (less than 1 hour) learning activity, and then returned one week later to complete the posttest. Depending on the experimental condition that each student was assigned to, they either completed only Proof Blocks problems, completed some Proof Blocks problems and some written proofs, or completed only written proofs for their learning activity. We find that students in the early phases of learning about proof by induction are able to learn just as much from reading lecture notes and using Proof Blocks as by reading lecture notes and writing proofs from scratch, but in far less time on task. This finding complements previous findings that Proof Blocks are useful exam questions and are viewed positively by students.

We introduce Analytic Program Repair, a data-driven strategy for providing feedback for type-errors via repairs for the erroneous program. Our strategy is based on insight that similar errors have similar repairs. Thus, we show how to use a training dataset of pairs of ill-typed programs and their fixed versions to: (1) learn a collection of candidate repair templates by abstracting and partitioning the edits made in the training set into a representative set of templates; (2) predict the appropriate template from a given error, by training multi-class classifiers on the repair templates used in the training set; (3) synthesize a concrete repair from the template by enumerating and ranking correct (e.g. well-typed) terms matching the predicted template. We have implemented our approach in Rite: a type error reporting tool for OCaml programs. We present an evaluation of the accuracy and efficiency of Rite on a corpus of 4,500 ill-typed Ocaml programs drawn from two instances of an introductory programming course, and a user-study of the quality of the generated error messages that shows the locations and final repair quality to be better than the state-of-the-art tool in a statistically-significant manner.

As dynamically-typed languages grow in popularity, especially among beginning programmers, there is an increased need to pinpoint their defects. Localization for novice bugs can be ambiguous: not all locations formally implicated are equally useful for beginners. We propose a scalable fault localization approach for dynamic languages that is helpful for debugging and generalizes to handle a wide variety of errors commonly faced by novice programmers. We base our approach on a combination of static, dynamic, and contextual features, guided by machine learning. We evaluate on over 980,000 diverse real user interactions across four years from the popular PythonTutor.com website, which is used both in classes and by non-traditional learners. We find that our approach is scalable, general, and quite accurate: up to 77% of these historical novice users would have been helped by our top-three responses, compared to 45% for the default interpreter. We also conducted a human study: participants preferred our approach to the baseline ($p = 0.018)$, and found it additionally useful for bugs meriting multiple edits.

This paper presents InFix, a technique for automatically fixing erroneous program inputs for novice programmers. Unlike comparable existing approaches for automatic debugging and maintenance tasks, InFix repairs input data rather than source code, does not require test cases, and does not require special annotations. Instead, we take advantage of patterns commonly used by novice programmers to automatically create helpful, high quality input repairs. InFix iteratively applies error-message based templates and random mutations based on insights about the debugging behavior of novices. This paper presents an implementation of InFix for Python. We evaluate on 29,995 unique scenarios with input-related errors collected from four years of data from Python Tutor, a free online programming tutoring environment. Our results generalize and scale; compared to previous work, we consider an order of magnitude more unique programs. Overall, InFix is able to repair 94.5% of deterministic input errors. We also present the results of a human study with 97 participants. Surprisingly, this simple approach produces high quality repairs; humans judged the output of InFix to be equally helpful and within 4% of the quality of human-generated repairs.

We introduce the FUSION algorithm for local refinement type inference, yielding a new SMT-based method for verifying programs with polymorphic data types and higher-order functions. FUSION is concise as the programmer need only write signatures for (externally exported) top-level functions and places with cyclic (recursive) dependencies, after which FUSION can predictably synthesize the most precise refinement types for all intermediate terms (expressible in the decidable refinement logic), thereby checking the program without false alarms. We have implemented FUSION and evaluated it on the benchmarks from the LiquidHaskell suite totalling about 12KLOC. FUSION checks an existing safety benchmark suite using about half as many templates as previously required and nearly 2 × faster. In a new set of theorem proving benchmarks FUSION is both 10 — 50 × faster and, by synthesizing the most precise types, avoids false alarms to make verification possible.

We present Refined TypeScript (RSC), a lightweight refinement type system for TypeScript, that enables static verification of higher-order, imperative programs. We develop a formal system for RSC that delineates the interaction between refinement types and mutability, and enables flow-sensitive reasoning by translating input programs to an equivalent intermediate SSA form. By establishing type safety for the intermediate form, we prove safety for the input programs. Next, we extend the core to account for imperative and dynamic features of TypeScript, including overloading, type reflection, ad hoc type hierarchies and object initialization. Finally, we evaluate RSC on a set of real-world benchmarks, including parts of the Octane benchmarks, D3, Transducers, and the TypeScript compiler. We show how RSC successfully establishes a number of value dependent properties, such as the safety of array accesses and downcasts, while incurring a modest overhead in type annotations and code restructuring.

A key challenge when statically typing so-called dynamic languages is the ubiquity of value-based overloading, where a given function can dynamically reflect upon and behave according to the types of its arguments. Thus, to establish basic types, the analysis must reason precisely about values, but in the presence of higher-order functions and polymorphism, this reasoning itself can require basic types. In this paper we address this chicken-and-egg problem by introducing the framework of two-phased typing. The first "trust" phase performs classical, i.e. flow-, path- and value-insensitive type checking to assign basic types to various program expressions. When the check inevitably runs into "errors" due to value-insensitivity, it wraps problematic expressions with DEAD-casts, which explicate the trust obligations that must be discharged by the second phase. The second phase uses refinement typing, a flow- and path-sensitive analysis, that decorates the first phase's types with logical predicates to track value relationships and thereby verify the casts and establish other correctness properties for dynamically typed languages.