Godel did not destroy formalization. He showed that there would always be true things that cannot be proved. It's true that the axioms used by Whitehead and Russell are not the axioms usually used today, but PM is still an important book that has influenced much work through today and Beyond. You might find this website interesting, which formalizes axioms and then proves many things from them: http://us.metamath.org/index.html