Discussion between user21820 and Nathaniel

Yes definitely. Almost any formal system that has been analyzed with modern mathematics requires manipulation of arbitrarily long strings.

@Nathaniel: You don't get my point. It's not a matter of whether you can prove ACA consistent. One might think ACA is consistent while ZFC is inconsistent, and so would more strongly believe certain theorems about certain programs than others. Are you really going to say you don't believe the Javascript program function(x){return x} captures the identity function on strings (given sufficient memory)? If you don't then please explain the empirical success of RSA decryption used in HTTPS world-wide.

@Nathaniel: That's right, but note that Presburger Arithmetic doesn't even have multiplication, so you won't be able to prove the correctness of RSA decryption. Furthermore, if you believe in the meaningfulness of the notion of formal systems, you essentially believe the basic properties of string manipulation, which is more or less equivalent to PA (see this post), or at least PA$^-$, which is finitely-axiomatized but essentially negation-incomplete. Rather deep is the rabbit-hole. =)