Wider Context

Code Extraction

Rocq can extract verified Gallina code to OCaml, Haskell, or Scheme. Enables running verified algorithms outside Rocq ecosystem. Trust required that extraction translation is correct.

Language Embedding

Embed target language (C, Java) and its semantics into Rocq. Prove programs correct with respect to embedded semantics. Trust required that semantics is correct and compiler enforces it.

Code Synthesis

Constructing programs automatically from specifications. Currently limited to small programs; active research area. Future direction for verification.

Self-Certification

Program produces result and separate checker verifies correctness. Examples: SAT solver produces model, verifier checks model; file download with checksum; sort with sortedness check. Checker can be formally verified.

Property-Based Testing

QuickCheck generates random test cases automatically from properties. prop_RevRev xs = reverse (reverse xs) == xs tested on 100 random lists. Finds edge cases unit testing misses.

Static Analysis

Compiler lints verify code satisfies specifications without execution. Example: clang-tidy detects potential null dereference when pointer usage depends on conditionals. Analyzes control flow statically.

Runtime Verification

Specify properties, monitor system during execution. Simple form: assert. Advanced: Address Sanitizer (memory errors), Undefined Behavior Sanitizer (UB detection), Thread Sanitizer (race conditions).

Strong Typing

Expressive type systems enforce invariants at compile time. Makes programs harder to write incorrectly. Dependent types can encode elaborate properties (e.g., sorted list).

Heavyweight vs Lightweight Verification

Heavyweight: formal verification with ITPs, very high confidence, expensive. Lightweight: testing, static analysis, runtime checks, less guarantee but practical.

Member Inductive Proposition

member n t defines when n appears in BST t. Constructors: leafmember (direct match), nodemember (root), leftmember/rightmember (recursive). Enables reasoning about tree membership.

Sorted BST Inductive Proposition

sorted t defines valid BST property. leafsorted: leaf always sorted. branchsorted requires: left and right sorted, all left members < n, all right members > n.

Verification Philosophy

Engineers have professional responsibility for quality. Formal verification provides mathematical certainty about correctness. Tooling exists to apply at scale