The equational and two column proof formats aren’t the same. Perhaps you should read Dijkstra’s monograph’s section on it to understand the differences. And to

The equational and two column proof formats aren’t the same. Perhaps you should read Dijkstra’s monograph’s section on it to understand the differences. And to say they are somehow isomorphic is to miss the point entirely. Sure “x is equal to y” means the same as “x = y”, but even the traditionalists recognize the merits of Recorde’s notational device, even if they fail to follow the greater implications thereof.