One more question I have is how PlusCal would fit into the picture. PlusCal was not existing when the TLA+ book was written. It seems that PlusCal would narrow the gap between a specification and a final implementation considerably, which might be a huge advantage in itself.