All are welcome to attend.
In recent years, there has been increased demand for computer science (CS) education at
the primary and secondary level. Traditionally, introductory CS courses teach students about an
imperative language, such as Java or Python, and students practice writing increasingly complex
programs from scratch. However, with the rise of AI-generated code, it is more important than
ever that students develop the skill of reasoning about unfamiliar code in a systematic and
critical manner. Additionally, many researchers have identified discrete mathematics courses as a
common difficulty for college computer science students due to students' unfamiliarity with
writing proofs. This work presents a 20-hour introductory computer science curriculum that aims
to address both of these problems. The course is tailored to high school students with little to no
coding experience, and it teaches students to code in OCaml and reason about program
correctness using equational reasoning and proof by induction. We incorporate modern
pedagogical techniques, including backward design, differentiated instruction, and
culturally-responsive pedagogy. This course not only prepares students for future work in
computer science but also strengthens the logical reasoning skills that math and science
disciplines require. This abridged course serves as a foundation for future proof-based
introductory computer science curricula.