- Author
- Not stated
- Published
- Undated (the page foot shows a 2026-08-24 timestamp)
- Kind
- Textbook chapter with exercises, from Software Foundations Volume 1
- Original
- softwarefoundations.cis.upenn.edu/lf-current/Basics.html
- Subject
- Formal methods and proof
What it is
The page is a chapter of an online course text, rendered from Rocq source. It sets out to teach Rocq's small functional language, called Gallina. The second half introduces tactics for proving properties of Gallina programs.
What it says
- The chapter says a side-effect-free procedure can be treated as a mathematical function. That link, it says, supports formal proofs and informal reasoning.
- The chapter says Rocq has very few built-in features. It builds days, booleans and numbers from scratch.
- Natural numbers are written with two constructors, O and S. The chapter says these names carry no meaning until functions use them.
- The chapter shows three ways to check examples. One of them extracts a program in OCaml, Scheme or Haskell.
- Unknown values block simplification, so proofs must consider the possible forms of a number. The destruct tactic splits a proof into those cases.
- An exercise formalizes a course late-day grading policy as functions. The chapter says the formalization exposes corner cases in the policy.
What evidence it gives
The chapter offers worked code, checked examples and proofs, and starred exercises with hints. Each chapter comes with test scripts that grade the exercises. The late-policy exercise applies the tools to a small, concrete rule set.
Interests and limits
Only the prose was read closely; code listings and some exercise text were skimmed. The page is a teaching text, so it makes few claims that could be tested. It teaches one tool, and its remarks on the wider field are brief.