The 1st order variant of the Dedekind/Peano theory of natural numbers is not suitable for computer science because it allows infinite integers and other monsters.

See the following: https://cacm.acm.org/blogs/blog-cacm/231495-what-turing-and-...