OCaml Crash Course
From Zero to Functional – OCaml for Verifiers & Solvers

by Yu Feng

OCaml: History & Industry Adoption
OCaml started in the late 1990s as a version of the Caml language, created by Xavier Leroy's team at INRIA in France. It comes from ML (Meta Language), which began in the 1970s. OCaml is an important step in the growth of typed functional programming languages.
Several versions have grown from OCaml. These include ReasonML from Facebook, which makes OCaml more like JavaScript; F# from Microsoft for .NET; and ReScript (once called BuckleScript), which turns OCaml into JavaScript.
Major Companies Using OCaml
Jane Street, a trading firm, built their entire trading system in OCaml and adds many tools to its community
Tech Companies
Facebook uses OCaml for tools like Hack, their PHP checker; Bloomberg uses OCaml for financial tools; and Docker was first built with OCaml
Research & Academia
Microsoft Research, INRIA, and many schools use OCaml for language research, checking program correctness, and building compilers
OCaml is fast, type-safe, and powerful, making it great for building complex systems where correctness matters most.
Core OCaml Syntax
Functional Language
Strong static types
Performance
ML + speed
Applications
Verifiers, interpreters, theorem provers
Let Bindings, Functions & Currying
let x = 3
let y = x + 1
let square x = x * x
let add x y = x + y
let add_curried = fun x -> fun y -> x + y
let add2 = add 2 (* partial application *)
Let Binds Names
Functions are values
Immutable Variables
By default
Curried Functions
Default in OCaml
If-Then-Else
let sign x = 
  if x > 0 then "positive"
  else if x < 0 then "negative"
  else "zero"
Expression-Based
If is an expression, not a statement
Type Consistency
All branches must return same type
Composable
Can be nested in other expressions
Tuples, Lists, and Pattern Matching
let pair = (3, "hello")
let (x, y) = pair
let lst = [1; 2; 3]
let rec sum xs = match xs with
  | [] -> 0
  | x :: xs' -> x + sum xs'
Tuples
Fixed-size, heterogeneous
Lists
Immutable, homogeneous
Pattern Matching
Core language construct
Option Type & Type Inference
let safe_div x y = 
  if y = 0 then None 
  else Some (x / y)

let b = true
let msg = "hello"
let double x = x * 2 (* inferred: int -> int *)
Why Option Types Matter: Option types provide a safe way to handle potentially missing values. Unlike languages that use null references, OCaml forces explicit handling of the None case, preventing runtime errors and making code more robust.
Some/None
Replaces null
Type Inference
Most types inferred statically
Safety
Prevents null pointer exceptions
Higher-Order Functions & Recursion
List.map (fun x -> x + 1) [1;2;3]
List.filter (fun x -> x mod 2 = 0) [1;2;3;4]
let rec factorial n = 
  if n = 0 then 1 
  else n * factorial (n - 1)
Functions as Values
Pass functions as arguments
Recursion
Primary control flow
No Loops
Recursion instead of iteration
Records, ADTs, and Recursive Evaluation
type student = { name: string; id: int }
type expr = 
  | Int of int 
  | Add of expr * expr 
  | Var of string

let rec eval e = match e with
  | Int n -> n
  | Add (e1, e2) -> eval e1 + eval e2
1
Records
Use for structs
2
ADTs
Algebraic Data Types
3
Pattern Matching
For ASTs and formulas
Variants & Enums
type logic_op = And | Or | Not
type result = Ok of int | Error of string
Variants provide type-safe enums and tagged unions
Matching Nested Data
type formula = True | Not of formula | And of formula * formula

let rec size f = match f with
  | True -> 1
  | Not f1 -> 1 + size f1
  | And (f1, f2) -> 1 + size f1 + size f2
Recursive Types
Self-referential data structures
Pattern Matching
Destructure complex data
Tree Traversal
Navigate nested structures
Assoc Lists and Base
let env = [("x", 3); ("y", 4)]
List.Assoc.find env "x" ~equal:String.equal
Assoc Lists
Simple key-value maps
Base Library
Standard library alternative
Lookups
Find values by key
Option Helpers & Errors
Option.value ~default:0 (Some 5)
Option.value_exn (Some 5)
failwith "something went wrong"
Default Values
Handle None cases gracefully
Exceptions
Extract values or fail
Error Handling
Raise exceptions when needed
ASTs for IMP
type aexp = 
  | Var of string | Int of int | Add of aexp * aexp
type formula = 
  | Eq of aexp * aexp | And of formula * formula
1
Abstract Syntax Trees
Represent program structure
2
Arithmetic Expressions
Variables, constants, operations
3
Formulas
Logical relationships
4
Recursive Structure
Nested expressions
SAT Formula Representation
type var = string
type literal = Pos of var | Neg of var
type clause = literal list
type formula = clause list
Z3 – Declaring Symbols
let ctx = Z3.mk_context []
let x = Z3.Arithmetic.Integer.mk_const_s ctx "x"
1
Create Context
Z3 solver environment
2
Declare Variables
Integer, Boolean, or other types
3
Build Expressions
Constraints using variables
Z3 – Building & Solving
let solver = Solver.mk_solver ctx None
let x_gt_1 = Arithmetic.mk_gt ctx x (Integer.mk_numeral_i ctx 1)
let _ = Solver.add solver [x_gt_1]
let result = Solver.check solver []
Create Solver
Initialize Z3 solver instance
Build Constraints
Define logical formulas
Add Assertions
Add constraints to solver
Check Satisfiability
Determine if constraints can be satisfied
Z3 – Reading Models
match Solver.get_model solver with
| Some model -> Model.to_string model
| None -> "unsat"
Get Model
Retrieve solution if satisfiable
Pattern Match
Handle sat/unsat cases
Extract Values
Read variable assignments
Recursive VCGen Example
let rec vcgen stmt post = 
  match stmt with
  | Skip -> post
  | Assign (x, e) -> substitute x e post
Verification Condition Generation
Transform programs to logical formulas
Substitution
Replace variables with expressions
Postconditions
Properties that must hold after execution
OCaml REPL (utop)
utop

# let x = 2 + 3;;
# List.map (fun x -> x * 2) [1;2;3];;
Interactive
Immediate feedback
Rich Features
Autocompletion, history, types
Experimentation
Try code snippets quickly
Project Setup with Dune
proj/
├── dune-project
├── src/
│   ├── main.ml
│   └── dune

(executable (name main))
Dune provides a standardized build system for OCaml projects
Build & Run
dune build
dune exec ./src/main.exe
Build Your Project
Compile all source files and dependencies with a single command
Execute Your Program
Run the compiled executable directly through Dune
Incremental Builds
Dune automatically tracks dependencies and rebuilds only what's necessary
Dune handles the entire build pipeline, from compiling modules to linking the final executable. The build system manages dependencies, parallel compilation, and proper rebuild ordering.
You're Ready!
OCaml syntax, recursion, pattern matching
How to write and evaluate ADTs
How to build SAT and VC tools
How to use Z3 in OCaml
🚀 Let's build something provably correct.