I'll assume that Bauer's not yet convinced you, even though you fully grok their examples. One application for computer scientists is to focus on computability

I'll assume that Bauer's not yet convinced you, even though you fully grok their examples. One application for computer scientists is to focus on computability of the real numbers. Turing's proof that there are uncomputable real numbers is nonconstructive, and it turns out that we can choose "all reals are computable" as an axiom of a topos. (This is the "Russian school" of constructive maths, ala Markov, IIUC.) This is "interesting and important" for both theory and engineering. For Poincaré-level mindblowing moments, we'll have to search across the landscape of topos theory, a landscape which was only dried out because of constructive maths damming up the floods of LEM and Choice. From homotopy type theory, we have the idea that types are like spaces; objects of the same type are related precisely by the possibility that one object might be deformable into the other. From higher category theory, we have the idea that sets are like 0-categories, and that set theory is just the bottommost slice of a 3D pyramid of category theories. Proving results neutrally to LEM and Choice is "not just stunts and gimmickry", because the proofs may be reused in any topos, and thus a neutral result is more true or less contextual than one which relies upon LEM. Bauer gives Johnstone, Diff, and RT as example topoi where LEM simply isn't true, but where neutral proofs would be reusable. Since RT is realizeable (by definition, it's the "realizability topos!") this means that neutral proofs each give runnable computer programs. This is sort of like beating Halo with only the pistol, and developing a sort of "pistol speedrun theory" where we study speedruns with games that have pistols. We aren't saying that there's not non-pistol speedruns, but emphasizing that pistols are a common feature. (Of course, the analogy breaks down here, since not all speedruns are pistol speedruns. Not all topoi are Grothendieck topoi, I suppose.)