Appendix F — Correctness by Construction: A Trade Lifecycle Proof

"The purpose of abstracting is not to be vague, but to create a new semantic level in which one can be absolutely precise." — E.W. Dijkstra

This appendix brings together the OCaml language features introduced throughout the book — phantom types, GADTs, algebraic effects, persistent data structures, and PPX metaprogramming — and demonstrates how they compose into a system where a large class of financial correctness properties are verified at compile time rather than runtime. The result is a trade lifecycle that is correct by construction: not correct because tests pass, but correct because incorrect programs cannot be compiled.

F.1 The Problem: Financial State Machine Bugs

A trade in a financial system has a lifecycle:

PENDING --[confirm]--> CONFIRMED --[allocate]--> ALLOCATED --[settle]--> SETTLED
                                       |
                              [reject] v
                               REJECTED

In traditional OOP implementations, lifecycle state is typically represented as a mutable enum field (trade.status = Status.CONFIRMED) or a string (trade.state = "confirmed"). Either approach suffers from the same defect: the compiler cannot distinguish a PENDING trade from a SETTLED trade. Any function that expects a settled trade can accidentally be called on a pending one. Unit tests catch this if someone writes the right test; the runtime catches it if someone adds the right assertion; the production system catches it when a client reports a ledger discrepancy.

OCaml eliminates this entire class of errors using the techniques in this book.

F.2 Phase 1 — Phantom-Typed Trade Lifecycle

State machine correctness is enforced at zero runtime cost using phantom types (Chapter 1, §1.2.1):

(** Phantom lifecycle state tags — no runtime values **)
type pending
type confirmed
type allocated
type settled
type rejected

(** A trade record parameterised by its phantom lifecycle state **)
type 'state trade = {
  trade_id    : string;
  instrument  : string;
  notional    : float;
  currency    : string;
  counterparty: string;
  trade_date  : string;
}

(** State transitions: type signatures encode the lifecycle graph **)
let confirm_trade (t : pending trade) : confirmed trade =
  (t :> confirmed trade)   (* same runtime layout; phantom changes *)

let allocate_trade (t : confirmed trade) : allocated trade =
  (t :> allocated trade)

let settle_trade (t : allocated trade) : settled trade =
  (t :> settled trade)

let reject_trade (t : confirmed trade) : rejected trade =
  (t :> rejected trade)

(** Only settled trades can generate ledger entries **)
let post_ledger_entry (t : settled trade) =
  Printf.printf "LEDGER: %.2f %s for %s on trade %s\n"
    t.notional t.currency t.counterparty t.trade_id

(** Only settled trades can be reported to regulators **)
let regulatory_report (t : settled trade) =
  Printf.printf "REG_REPORT: trade=%s notional=%.2f\n" t.trade_id t.notional

The compiler rejects any attempt to call post_ledger_entry on a pending trade or confirmed trade. The lifecycle is enforced without a single runtime check, enum comparison, or defensive assertion. These invariants hold on every code path for every trade, in every deployment, forever — not just in code paths covered by tests.

F.3 Phase 2 — Currency-Safe Notional Arithmetic

Trade notionals carry a currency. Adding GBP notional to USD notional is a silent error in most systems. Phantom types extend to multi-currency books:

(** Currency tags **)
type usd
type eur
type gbp
type jpy

(** Currency-tagged notional **)
type 'ccy notional = Notional of float

(** FX rate encodes the conversion direction in both type parameters **)
type ('from, 'to_) fx_rate = FxRate of float

(** Currency-safe trade with phantom currency tag **)
type ('state, 'ccy) trade_ccy = {
  trade_id   : string;
  instrument : string;
  notional   : 'ccy notional;
  currency   : string;
  counterparty: string;
}

(** Add two notionals: only compiles if same currency **)
let add_notionals (Notional a : 'ccy notional) (Notional b : 'ccy notional)
    : 'ccy notional = Notional (a +. b)

(** Convert: requires explicit FX rate with correct direction **)
let convert_notional (FxRate r) (Notional a : 'from notional)
    : 'to_ notional = Notional (a *. r)

(** Example: USD book aggregation **)
let aggregate_usd_book (trades : (settled, usd) trade_ccy list) : usd notional =
  List.fold_left
    (fun acc t -> add_notionals acc t.notional)
    (Notional 0.0)
    trades
  (* ^^^ compile-time error if any trade has currency != usd *)

F.4 Phase 3 — GADT-Encoded Instrument Pricing

Once a trade is typed with its lifecycle state and currency, we need to price the underlying instrument. GADTs (Chapter 2, §2.10) encode the mapping from instrument to pricing result:

(** GADT: each constructor specifies what pricing returns **)
type 'a instrument =
  | Equity_option : {
      underlying : string;
      strike     : float;
      expiry     : float;
      kind       : [`Call | `Put];
    } -> float instrument                    (* single price **)
  | Interest_rate_swap : {
      fixed_rate : float;
      float_rate : float;
      notional   : float;
      tenor      : float;
    } -> (float * float) instrument          (* (pv, dv01) **)
  | Credit_default_swap : {
      reference  : string;
      spread_bps : float;
      maturity   : float;
      notional   : float;
    } -> (float * float) instrument          (* (pv, cs01) **)

(** Returns the correct type for each instrument — verified by compiler **)
let price_instrument : type a. a instrument -> a = function
  | Equity_option { strike; expiry; kind; _ } ->
    let s = 100.0 and r = 0.05 and v = 0.20 in
    (match kind with
     | `Call -> Black_scholes.call ~spot:s ~strike ~rate:r ~vol:v ~tau:expiry
     | `Put  -> Black_scholes.put  ~spot:s ~strike ~rate:r ~vol:v ~tau:expiry)
  | Interest_rate_swap { fixed_rate; float_rate; notional; tenor } ->
    let pv  = notional *. (fixed_rate -. float_rate) *. tenor in
    let dv01 = notional *. tenor *. 0.0001 in
    (pv, dv01)
  | Credit_default_swap { spread_bps; notional; maturity; _ } ->
    let pv   = notional *. spread_bps /. 10000.0 *. maturity in
    let cs01 = notional *. maturity *. 0.0001 in
    (pv, cs01)

F.5 Phase 4 — Effects for Pricing Context

The pricing function above uses hardcoded spot prices. In production it must fetch market data from a source that varies by context (live, backtest, stress). Effects (Chapter 2, §2.11) provide this without parameter threading:

(** Market data effects **)
effect Get_spot   : string -> float
effect Get_vol    : string -> float
effect Get_rate   : string -> float

(** Rewritten pricer: requests data from the effect handler **)
let price_option_with_effects ~ticker ~strike ~expiry ~kind =
  let spot = perform (Get_spot ticker) in
  let vol  = perform (Get_vol  ticker) in
  let rate = perform (Get_rate "USD")  in
  (match kind with
   | `Call -> Black_scholes.call ~spot ~strike ~rate ~vol ~tau:expiry
   | `Put  -> Black_scholes.put  ~spot ~strike ~rate ~vol ~tau:expiry)

(** Handler 1: live production data **)
let run_live f =
  match f () with
  | v -> v
  | effect (Get_spot ticker) k -> continue k (Market_feed.spot ticker)
  | effect (Get_vol ticker)  k -> continue k (Market_feed.vol ticker)
  | effect (Get_rate ccy)    k -> continue k (Market_feed.rate ccy)

(** Handler 2: stress scenario — equity down 20% **)
let run_equity_crash f =
  match f () with
  | v -> v
  | effect (Get_spot ticker) k -> continue k (Market_feed.spot ticker *. 0.80)
  | effect (Get_vol ticker)  k -> continue k (Market_feed.vol ticker *. 1.50)
  | effect (Get_rate ccy)    k -> continue k (Market_feed.rate ccy)

(** Same pricing code, three different contexts **)
let live_price   = run_live         (fun () -> price_option_with_effects ~ticker:"AAPL" ~strike:150.0 ~expiry:1.0 ~kind:`Call)
let crash_price  = run_equity_crash (fun () -> price_option_with_effects ~ticker:"AAPL" ~strike:150.0 ~expiry:1.0 ~kind:`Call)

F.6 Phase 5 — PPX for Serialisation and Reporting

Trade records must be serialised to databases, risk systems, and regulatory reports. PPX derivations (Chapter 2, §2.13) automate this from type definitions:

(** Complete trade record with PPX-derived serialisation **)
type trade_record = {
  trade_id        : string;
  instrument      : string;
  notional        : float;
  currency        : string;
  counterparty    : string;
  trade_date      : string;
  lifecycle_state : [`Pending | `Confirmed | `Allocated | `Settled | `Rejected];
  price           : float option;
} [@@deriving show, compare, equal, yojson, bin_io]

(** Generated functions:
    show_trade_record      : trade_record -> string
    compare_trade_record   : trade_record -> trade_record -> int
    equal_trade_record     : trade_record -> trade_record -> bool
    trade_record_to_yojson : trade_record -> Yojson.t
    trade_record_of_yojson : Yojson.t -> trade_record result
    bin_write_trade_record : Bin_prot.Write.writer  <-- microsecond-latency binary **)

(** Regulatory report serialisation — no hand-written formatters **)
let export_trades_json trades =
  `List (List.map trade_record_to_yojson trades)
  |> Yojson.Safe.to_string

F.7 The Complete Picture

The full system composes these five independently useful features into a single correctness guarantee:

None of these features is a workaround or a patch. Each is an idiomatic OCaml pattern, composable with all the others, and available in every OCaml program without additional dependencies. Together, they form a system where the type-checker is a collaborator, not just a spell-checker: it actively verifies that the program obeys its contracts at every call site, for every state, for every instrument, in every market condition.

This is the fundamental distinguishing property of OCaml for quantitative finance. Python, Java, and C++ finance libraries provide correct behaviour under the code paths developers test. An OCaml library that uses these patterns provides correct behaviour under all code paths that the compiler accepts — because incorrect code paths are rejected before the program runs.

F.8 Summary of Language Features by Use Case

Back to Summary