C+

Examples

Real programs and proof recipes

Complete C+ programs and focused proof recipes you can build, check, or run yourself. Each one ships the source, an explanation of what it proves, the result to expect, and the exact steps to reproduce it.

Ray tracer

Graphics

A complete path tracer in one C+ file: 10 spheres with Lambertian, metal, and dielectric materials, rendered to a PPM image. Full source, a walkthrough, the numbers it produces, and how to reproduce them.

A proven allocation-free control kernel on the ESP32

Embedded

C+ proves an embedded control kernel never allocates or blocks before any firmware is flashed. A fixed-point PID step marked #[realtime], cross-compiled to the ESP32, with the contract checked across the whole call graph at cpc check time.

Realtime audio meter

Realtime

A small audio-style hot path that is accepted under #[realtime], plus negative fixtures that prove hidden allocation, blocking, and oversized stack frames are rejected by the compiler.

A native iOS screen in C+

iOS

A native iOS app whose UI is written in C+: a UIWindow with a centered label, built through the uikit bindings, cross-compiled with cpc, linked by Xcode, and rendered on the iPhone simulator. The only C is a two-line main shim.

AppKit agent surface

Agent UI

The checked appkit_agent recipe from the C+ source tree: a macOS AppKit window exposed through agent_appkit and agent_mcp, with tagged controls, consent-gated JSON-RPC actions, and stale text rejection.

AppKit hello

GUI

The checked appkit_hello recipe from the C+ source tree: a native macOS AppKit window, typed controls, C+ Text to NSString bridging, a Quit callback, and the real AppKit event loop.

Build a construction DSL with @ctx

Language

Create your own declarative DSL in a few lines: a package that ships the Builder protocol, then a @ctx { ... } block that uses it — with modifiers, a setup let, and a container. No macros; it lowers to ordinary calls.

C ABI consumer

FFI

The checked c_consumer reference example from the C+ source tree: build a C+ library, generate a C header, link it from C, and exercise scalar, struct, enum, pointer, and function-pointer ABI classes.

SIMD dot product

SIMD

The checked simd_dot recipe from the C+ source tree: compare a scalar dot product with an explicit f32x4 FMA loop and exit 0 only when both produce 347.

Metal compute

GPU

The macOS-only metal_compute reference recipe from the C+ source tree: compile a Metal shader, embed the metallib, dispatch it through Objective-C FFI, and verify GPU readback.

Threads and atomics

Concurrency

The checked parallel_sum and concurrent_counter recipes from the C+ source tree: partition-and-join threading, plus the explicit atomic pattern for shared mutable state.

Async / await

Async

Checked async recipes from the C+ source tree: chained async fn + await, cooperative spawn_local/yield_now, and method-form async TCP I/O driven by executor::block_on.