We report on a prototype small tutoring program run entirely within the existing undergraduate teaching assistant (TA) staff of a large (around 600 students) first semester Computer Science class with an equally large (around 80) staff of undergraduate TAs. The tutoring team, led by the second, third, and fourth authors (all undergraduate TAs), identified students who could benefit from the service by analyzing existing course assessments (homework, labs, and exams), some of which were slightly modified to aid this task.

This paper describes FEEDBOT, an open-source formative assessment tool leveraging large language models (LLMs) to provide structured, high-level feedback on design-oriented programming assignments. Designed to address the limitations of traditional autograding and overcome scaling challenges of formative assessment, FEEDBOT uses an existing pedagogical framework to provide targeted but limited actionable feedback. Early results demonstrate measurable improvements in student performance in a large introductory computer science course, while avoiding the pitfall of providing too much assistance that more unstructured tools commonly encounter. Although this experience report focuses on a particular implementation, we believe that FEEDBOT (and its general approach) is adaptable to many other contexts.

A course on software specification deserves a prominent place in the undergraduate curriculum. This report describes our experience teaching a first-year course that places software specification front and center. In support of the course, we created a pedagogic programming language with a focus on contracts and propertybased testing. Assignments draw on real-world programs, from a variety of domains, that are intended to show how formal specification can increase confidence in the correctness of code. Interviews with students suggest that this approach successfully conveys how formal specification is relevant to software construction.

Programs are rarely implemented in a single language, and thus questions of type soundness should address not only the semantics of a single language, but how it interacts with others. Even between type-safe languages, disparate features can frustrate interoperability, as invariants from one language can easily be violated in the other. In their seminal 2007 paper, Matthews and Findler proposed a multi-language construction that augments the interoperating languages with a pair of boundaries that allow code from one language to be embedded in the other. While this technique has been widely applied, their syntactic source-level interoperability doesn’t reflect practical implementations, where the behavior of interaction is only defined after compilation to a common target, and any safety must be ensured by target invariants or inserted target-level “glue code.”

Compiler correctness is an old problem, with results stretching back beyond the last half-century. Founding the field, John McCarthy and James Painter set out to build a "completely trustworthy compiler". And yet, until quite recently, even despite truly impressive verification efforts, the theorems being proved were only about the compilation of whole programs, a theoretically quite appealing but practically unrealistic simplification. For a compiler correctness theorem to assure complete trust, the theorem must reflect the reality of how the compiler will be used. There has been much recent work on more realistic "compositional" compiler correctness aimed at proving correct compilation of components while supporting linking with components compiled from different languages using different compilers. However, the variety of theorems, stated in remarkably different ways, raises questions about what researchers even mean by a "compiler is correct." In this pearl, we develop a new framework with which to understand compiler correctness theorems in the presence of linking, and apply it to understanding and comparing this diversity of results. In doing so, not only are we better able to assess their relative strengths and weaknesses, but gain insight into what we as a community should expect from compiler correctness theorems of the future.

We present FunTAL, the first multi-language system to formalize safe interoperability between a high-level functional language and low-level assembly code while supporting compositional reasoning about the mix. A central challenge in developing such a multi-language is bridging the gap between assembly, which is staged into jumps to continuations, and high-level code, where subterms return a result. We present a compositional stack-based typed assembly language that supports components, comprised of one or more basic blocks, that may be embedded in high-level contexts. We also present a logical relation for FunTAL that supports reasoning about equivalence of high-level components and their assembly replacements, mixed-language programs with callbacks between languages, and assembly components comprised of different numbers of basic blocks.

Computing educators have used peer review in various ways in courses at many levels. Few of these efforts have applied peer review to multiple deliverables (such as specifications, tests, and code) within the same programming problem, or to assignments that are still in progress (as opposed to completed). This paper describes CaptainTeach, a programming environment enhanced with peer-review capabilities at multiple stages within assignments in progress. Multi-stage, in-flow peer review raises many logistical and pedagogical issues. This paper describes CaptainTeach and our experience using it in two undergraduate courses (one first-year and one upper-level); our analysis emphasizes issues that arise from the conjunction of multiple stages and in-flow reviewing, rather than peer review in general.

We present a small-step operational semantics for the Python programming language. We present both a core language for Python, suitable for tools and proofs, and a translation process for converting Python source to this core. We have tested the composition of translation and evaluation of the core for conformance with the primary Python implementation, thereby giving confidence in the fidelity of the semantics. We briefly report on the engineering of these components. Finally, we examine subtle aspects of the language, identifying scope as a pervasive concern that even impacts features that might be considered orthogonal.