My work consists of denotational semantics for a first-order differentiable programming language which has smooth manifolds as ground types. It supports basic data types, partiality, conditionals, and iteration. The typing judgments also tracks the differentiability class of terms. The semantics uses a family of restriction categories and a kind of lax functor between them. It also validates relations often used by automatic differentiation implementations.