CZF is Peter Aczel's constructive set theory, his compromise
between the familiar yet "cloudy" language of ZF and the
concrete yet "scratchy" bedrock of intuitionistic type theory.
In this introductory talk, I will walk through the development of CZF,
starting at the very bottom---with the well-founded-tree construction
that grounds everything in computational type theory---and working
up through the basic propositions to the ZF-like axioms.