Update: added custom functions.

Since version 2.0 is out (has been for a while actually) a small update.
A bunch of features that never really worked well are not in 2.0, such as functions, let-guards (what even are those, you're probably wondering), solve-with-arguments/universal quantification and the weirdest feature ever, "loop".

They probably won't be back, unless anyone complains. No one used them except to try them out. Solve-with-arguments was actually quite powerful, but I guess no one understood what it does (I'm not sure I understand it myself tbh), annoying to implement though.

The SAT part doesn't work properly so if you use queries that are too hard for BDDs it will just fail in some obscure way.

It's symbolic, it can do concrete calculations too, that's necessary of course but also in a way a side effect of the symbolic engine. It's not terribly useful as Plain Old Calculator though.

The bot on OIRC is dead because I lost my nice host that would let me run an IRC bot, I could find a new host I guess, but it wouldn't be the same as the website any more (it used to be the same program running the site and the IRC bot, though in IRC mode it kept its output short). The website is purely client side now, makes it a lot easier to find free hosts. So it's all in JS now, no more Java. I could dig up my little project to use Eeems' JS bot-framework with haroldbot, and then I'd still have to host it somewhere.. it could be done

Everyday's life problems though, I think that's more something for wolfram alpha. But perhaps I can explain just what it is that haroldbot does, without going too far into the technical details.

The fundamental difference between haroldbot and the average symbolic math thing is that it works with 32 bit integers. The usual tools typically have no (easy) way to do that (WA can do some of it, but it's awkward), but I needed it, so I filled the gap. This directly results in, for example, x == -x having the solution 0x80000000 as well as the usual 0, and x*3 == 1 having the solution x=0xAAAAAAAB.
The most important use case is testing whether two expressions (with variables in them) are equivalent, with all the math still being doing on 32 bit integers, so it can be useful when debugging some weird bithack you thought of. It can even give a proof in some cases (usually not), which serves two purposes: show that it didn't just lie (the steps can be checked, if it just said "well, they're equal" it's harder to trust that it's right) and, sometimes, show why something is true (for sufficiently legible proofs).

Can someone explain why ""0x80000000 / -1" in signed mode" should error?

...
On the other hand, 0x80000000 is a fairly legitimate result for 0x80000000 / -1, because -0x80000000 = 0x80000000.

Well, it depends on your definition of legitimate. As you know, in (32-bit) two's complement notation, the maximal positive number is 0x7FFFFFFF and the minimal number is 0x80000000. So, -0x80000000 = 2147483648 does not really exist as a positive number.  I don't think this is arithmetically legitimate and you should handle the overflow exception. Or do you mean a possible value?