mathlib

df450024 - feat(archive): formalize compiler correctness by McCarthy and Painter (#4702)

feat(archive): formalize compiler correctness by McCarthy and Painter (#4702) Add a formalization of the correctness of a compiler from arithmetic expressions to machine language described by McCarthy and Painter, which is considered the first proof of compiler correctness.