Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

BOOP: Write Right Code

Vaani Goenka, Aalok Thakkar

TL;DR

The paper addresses the challenge that novice programmers often rely on syntax-specific, test-driven methods, a tendency amplified by AI coding tools. It introduces BOOP (Blueprint, Operations, OCaml, Proof), a four-phase, correctness-first pedagogy implemented via a preprocessor and VS Code extension to enforce formal specifications, language-agnostic algorithms, implementations, and proofs. Early evaluations at Ashoka University show improvements in algorithmic reasoning, edge-case understanding, and problem decomposition, with instructors observing stronger foundational skills despite some initial perception of verbosity. The work suggests that a structured correctness-first approach can meaningfully boost computational thinking and offers a roadmap for integrating formal methods, automated verification, and broader institutional deployment.

Abstract

Novice programmers frequently adopt a syntax-specific and test-case-driven approach, writing code first and adjusting until programs compile and test cases pass, rather than developing correct solutions through systematic reasoning. AI coding tools exacerbate this challenge by providing syntactically correct but conceptually flawed solutions. In this paper, we address the question of developing correctness-first methodologies to enhance computational thinking in introductory programming education. To this end, we introduce BOOP (Blueprint, Operations, OCaml, Proof), a structured framework requiring four mandatory phases: formal specification, language-agnostic algorithm development, implementation, and correctness proof. This shifts focus from making the code to understanding the code is correct. BOOP was implemented at Ashoka University using a VS Code extension and preprocessor that enforces constraints. Initial evaluation shows improved algorithmic reasoning and reduced trial-and-error debugging. Students reported better edge case understanding and problem decomposition, though some initially found the format verbose. Instructors observed stronger foundational skills compared to traditional approaches, suggesting that structured correctness-first approaches may significantly improve students' computational thinking abilities.

BOOP: Write Right Code

TL;DR

The paper addresses the challenge that novice programmers often rely on syntax-specific, test-driven methods, a tendency amplified by AI coding tools. It introduces BOOP (Blueprint, Operations, OCaml, Proof), a four-phase, correctness-first pedagogy implemented via a preprocessor and VS Code extension to enforce formal specifications, language-agnostic algorithms, implementations, and proofs. Early evaluations at Ashoka University show improvements in algorithmic reasoning, edge-case understanding, and problem decomposition, with instructors observing stronger foundational skills despite some initial perception of verbosity. The work suggests that a structured correctness-first approach can meaningfully boost computational thinking and offers a roadmap for integrating formal methods, automated verification, and broader institutional deployment.

Abstract

Novice programmers frequently adopt a syntax-specific and test-case-driven approach, writing code first and adjusting until programs compile and test cases pass, rather than developing correct solutions through systematic reasoning. AI coding tools exacerbate this challenge by providing syntactically correct but conceptually flawed solutions. In this paper, we address the question of developing correctness-first methodologies to enhance computational thinking in introductory programming education. To this end, we introduce BOOP (Blueprint, Operations, OCaml, Proof), a structured framework requiring four mandatory phases: formal specification, language-agnostic algorithm development, implementation, and correctness proof. This shifts focus from making the code to understanding the code is correct. BOOP was implemented at Ashoka University using a VS Code extension and preprocessor that enforces constraints. Initial evaluation shows improved algorithmic reasoning and reduced trial-and-error debugging. Students reported better edge case understanding and problem decomposition, though some initially found the format verbose. Instructors observed stronger foundational skills compared to traditional approaches, suggesting that structured correctness-first approaches may significantly improve students' computational thinking abilities.

Paper Structure

This paper contains 26 sections, 2 theorems.

Table of Contents

  1. Introduction
  2. Related Work
  3. Functional Programming Education
  4. AI and CS Pedagogy
  5. Pattern-Based Approaches to Programming Education
  6. Correctness-by-Construction
  7. Overview
  8. Three Incorrect Approaches
  9. Pedagogical Analysis
  10. Blueprint Specification
  11. Algorithm as Operations
  12. Proof of Correctness
  13. The BOOP Framework for Systematic Problem-Solving
  14. The Four-Phase BOOP Framework
  15. Enforcement Through Technical Infrastructure
  16. ...and 11 more sections

Key Result

theorem thmcountertheorem

The function in lst:overview-div correct; that is, for given natural numbers and :

Theorems & Definitions (3)

  • theorem thmcountertheorem
  • theorem thmcountertheorem
  • proof