WHAT IS...a Topos ?
Luc Illusie
http://www.ams.org/notices/200409/what-is-illusie.pdf

In the last remark about the "extensive use of elementary topoi in logic",
he might have added that they have been used to prove
the independence of Axiom of Choice, and that also they are now used
in computer science (I am not sure why, though...)

http://gavrilov.akatov.com/forum/viewforum.php?f=5