Automation is not a proof of correctness. It is a proof of translation. When reading about Fuzzi, a three-level logic for differential privacy, there is a temptation to see it as a bridge that finally solves the tension between rigid type systems and manual program logics.