Occam-pi and KRoC are the result of on-going research extending the (CSP) ideas of occam by judicious inclusion of the mobility features of the pi-calculus. In the interests of proveability, we have been careful to preserve the distinction between the original simple static point-to-point synchronised communication of occam and the dynamic asynchronous multiplexed communication of the pi-calculus; in this we have been prepared to sacrifice the elegant sparsity of the pi-calculus. We conjecture that the extra complexity (and discipline) introduced will make the task of proving concurrent and distributed programs easier.