Formal systems aren't just about mechanizing mathematical work to make it a subject of software engineering. (Though this is a useful and probably underdeveloped outcome.) They also turn mathematical work itself into mathematical objects which one can reason about, which opens the door to metamathematics, i.e. the ability to reason mathematically about aspects of mathematics itself.