Comment by TimorousBestie

In addition to these points we also have a handful of weaker-than-arithmetic but provably-decidable theories, which jointly encompass almost everything done on a finite computer.