What is the computational substance of the axiom of choice?

This post is also available on my Substack.I feel like online discussions of the axiom of choice either get impenetrably technical, or uselessly vague. Through realizability semantics, I’ve gotten an intuition for the axiom of choice that I want to share in elementary terms (without getting all the way into the effective topos). I will take a somewhat eccentric approach to it, showing the everyday utility of the axiom of choice, as well as the implications from a constructive rather than a class...