It wasn't stopped, it's just way, way harder than one would naively expect. Russell continued to work on it by developing type theory, which was later carried on by people like Alonzo Church and Per Martin-Löf. This led not just to types in programming, but also to the use of types in proof checkers like Coq and Agda, which are very much the kind of thing you're talking about. Efforts are ongoing to continue working towards the vision of automated theorem proving, but again, it is an extremely difficult problem.