[vosper]

I read it as they're talking about making proof assistants practical one day, and CakeML is a step on the road to that goal. If they then move onto the next step, where does that leave CakeML?