There's a tendency in proof theory circle to dismiss set theory and related foundational work, yet it is ultimately the basis that is used (other foundational p

There's a tendency in proof theory circle to dismiss set theory and related foundational work, yet it is ultimately the basis that is used (other foundational programs with 'better properties' tend to have worse issues). So it's not necessarily a dig towards Gödel, but to show that the book would be dismissed, without any dig to living logicians. But the reason would be that you find better and easier introductions to the material, where you don't have to internally translate to their more idiosyncratic syntax. Such a project is not going to give it mass appeal, but make it a tad more approachable for highly motivated people.