Abstract: It can be a problem in the theory of the $\pi$-calculus that a process $P$, such as $P=\nu b.a!b$ (restrict $b$ in output $b$ along $a$) can undergo infinitely many different transitions, one for each fresh $b$. Theoretical treatments usually come with $\alpha$-equivalence results to show that they only need to consider one of these fresh names. They are specific to the theorem of interest; a general formal treatment of why such results hold is lacking, as is a programming framework for them. FreshML is a dialect of ML with an abstraction type-former which supplies such a programming framework. Given a type $X$ and a type of names $\text{Atoms}$, $<\text{Atoms}>X$ is the type of elements of $X$ with a name in $\text{Atoms}$ bound. If $\Pi$ is a datatype of $\pi$-calculus processes and $L$ a datatype of labels, the type $\Pi *<\text{Atoms}>(L*\Pi )$ models $\pi$-calculus transitions. The bound name is a fresh name if the transition generates one. For example: $(\nu b.a!b,<b>(a!b,0))$ represents the transition(s) $\nu b.a!b-a!(b)->0$. We find that the programming principles associated to such datatypes model our hitherto informal understanding of names and binding. Thus FreshML is an intuitive tool. I shall give some theory, show some programs, and discuss how they work.