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.

A Facet counter on AppKit

macOS

A C+ 0.0.28 Facet application using the named-window runtime and native AppKit backend: component state, a keyed label, and a button handler.

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.

AppKit agent surface

Agent UI

A macOS AppKit window exposed through agent_appkit and agent_mcp, with tagged controls, capability grants, 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: compiler-driven async entry points, chained await, cooperative spawn_local/yield_now, and method-form async TCP I/O.

A native iOS screen in C+

Later

A native iOS app whose UI is written in C+ through UIKit, cross-compiled as an archive and header for Xcode to link.