Desktop-manufacturing techniques like 3D printing are increasingly
popular because they reduce the cost and complexity of producing
customized objects on demand. Unfortunately, the vibrant communities of
early adopters, often referred to as “makers,” are not well-served by
currently available software pipelines. Users today must compose
idiosyncratic sequences of tools which are typically repurposed variants
of proprietary software originally designed for expert specialists.

This paper proposes fundamental programming-languages techniques to
bring improved rigor, reduced complexity, and new functionality to the
computer-aided design (CAD) software pipeline for applications like
3D-printing. Compositionality, denotational semantics, compiler
correctness, and program synthesis all play key roles in our approach,
starting from the perspective that solid geometry is a programming
language.

Specifically, we define a purely functional language for CAD called lcad
and a polygon surface-mesh intermediate representation. We then define
denotational semantics of both languages to 3D solids and a compiler
from CAD to mesh accompanied by a proof of semantic preservation. We
illustrate the utility of this foundation by developing a novel
synthesis algorithm based on evaluation contexts to “reverse compile”
difficult-to-edit meshes downloaded from online maker communities back
to more-editable CAD programs. All our prototypes have been implemented
in OCaml modularly to enable further exploration of functional
programming for desktop manufacturing.