A Correctness-First Introduction to Computer Science

Abstract

Introductory computer science courses commonly use programming for instruction and assessment. This has several weaknesses because working code is not a reliable proxy for complete understanding. Elements of instruction – mathematics, a specific programming language, syntax, test-cases – all come together to conflate the boundaries and the specific purposes of these tools. We propose a correctness-first pedagogical framework for introductory computer science that separating semantic reasoning from syntactic implementation. The framework structures problem solving into four epistemic stages: blueprint specifications expressed as pre- and postconditions, natural-language operational steps that make program behaviour explicit, code implementation, and proof of correctness. Central to this approach is a natural-language intermediate layer that enables students to reason about computation independently of programming syntax, making formal correctness reasoning accessible in early coursework. We describe BOOP, a tool that implements this framework through lecture-integrated workflows and assignment support. BOOP is delivered via a web-based IDE and a VS Code extension, and provides automated checking of loop invariants and specifications. We report on a classroom deployment across two semesters (48 students). Qualitative analysis indicates earlier and more explicit engagement with correctness criteria, improved handling of edge cases, and increased willingness to reason beyond test inputs. Our results suggest that correctness-first instruction is both pedagogically feasible in introductory CS courses and necessary for realigning assessment practices with foundational computational thinking goals in the presence of increasingly capable code-generation tools.