For the same reason mathematicians who aren't computer scientists or logicians are attracted to proof assistants implementing ZFC object languages while ignoring the stuff underneath (type theory, systems theory, etc.)