A realizability topos is the exact completion of a category of assemblies. If I understood correctly, the major achievement of the completion is having (1) subobject classifier and (2) finite colimits, including coequalizers of equivalence relations.
However, a category of assemblies seems rich enough to model (certain) constructive dependent type theories with a straightforward interpretation: terms to computable functions and types to data types (assemblies).
I was wondering then what the main motivation and advantage of inventing this completion, having subobject classifier and quotients, and working with realizability topos instead of a category of assemblies are.
Will there be some illuminating examples that can only be done in a realizability topos but not in a category of assemblies?