I am a big proponent of computer algebra systems (in particular Sage) and I know that I use sage a lot in my day to day research. When I'm learning a new branch of math, I like to see what packages are available for working with that branch of math, and I was surprised by how little set theory is available. Sure there are packages for working with sets, but nothing more advanced than unions, intersections, etc.
Obviously there are certain things in set theory that it would be unreasonable to ask a computer to do (show each partial function in a definition by recursion, if you want a function on some infinite ordinal at the end) but there are things that I think would be extremely helpful to those learning the field, if not to researchers. We as mathematicians are able to work in a finite metatheory, so there's no immediate reason why computers could not also reason about infinite cardinals, say, in the same way.
Why, then, are there no packages (or, at least, very few packages) for working with forcing posets, large cardinals, or even working with basic model theory? As a second, related question, are there small computable examples to work with? How do you test if your theorem is actually true? I trust my proofs, but it always feels nice when you actually compute something and you get the expected answer. Sage is such an integral part of "checking my work" that I'm not sure how I would go about doing research in a field without it.
Sorry if this is a naïve question, and thanks in advance for any answers ^_^