@whitequark@mastodon.social I'd say it's a path to formally verified optimization - but that has zero benefits until there's formal verification for the rest of compilation