10 · Autodiff

Mark a function @differentiable and the compiler generates its derivative automatically — no symbolic math library, no numerical finite-differences. The ∂ operator returns the derivative of a differentiable function; ∂∂ gives the second derivative. Both forward and reverse mode are available and the mode is selected by the compiler based on the shape of the computation.

autodiff.cssl

// The compiler generates ∂(square) alongside square.
@differentiable
fn square(x: f32) -> f32 {
    x * x
}

// Multi-variable — partial derivatives available via ∂.
@differentiable
fn poly(x: f32, y: f32) -> f32 {
    x * x + 2.0 * x * y + y * y
}

fn main() !io {
    let x = 3.0_f32;

    // Forward evaluation.
    println!("square(3)     = {}", square(x));      // 9

    // First derivative at x = 3: d/dx (x²) = 2x = 6.
    println!("∂square(3)    = {}", ∂(square)(x));   // 6

    // Second derivative: d²/dx² (x²) = 2.
    println!("∂∂square(3)   = {}", ∂∂(square)(x));  // 2

    // Partial derivative ∂poly/∂x at (1, 2): 2x + 2y = 6.
    println!("∂ₓpoly(1,2)   = {}", ∂ₓ(poly)(1.0, 2.0)); // 6

    // Partial derivative ∂poly/∂y at (1, 2): 2x + 2y = 6.
    println!("∂ᵧpoly(1,2)   = {}", ∂ᵧ(poly)(1.0, 2.0)); // 6
}

Output

square(3)     = 9
∂square(3)    = 6
∂∂square(3)   = 2
∂ₓpoly(1,2)   = 6
∂ᵧpoly(1,2)   = 6

What the compiler sees

@differentiable is a compiler directive, not a runtime annotation. The compiler analyzes the function body, applies the chain rule symbolically, and emits the derivative as a separate callable. Functions that branch on a differentiable variable produce subgradients at non-smooth points. Non-differentiable operations (integer casts, bit ops) inside an @differentiable function are a compile error. See §C.1 Autodifferentiation for forward vs. reverse mode selection rules.

---

Next → 11 · SMT Verification