Hoare logic is bedevilled by complex and unmemorable
side conditions on the use of variables. We define a logic
free of side conditions, and show that it admits translations
of proofs in Hoare logic, thereby showing that nothing is
lost. Our work draws on ideas from separation logic: program
variables are treated as resource and separated with
?, rather than as logical variables in disguise. For clarity
we exclude a treatment of the heap.