Yeah, it’s really neat seeing mainstream mathematicians finally applying mathematical methods computing scientists discovered half a century ago.

The isomorphism between programs and proofs implies we’ll see this or similar techniques developed for constructing programs that can be readily mathematically reasoned about applied more and more often in different areas. Good stuff.