You are quite right: Smalltalk is not a systems programming language, so no operating systems nor device drivers.
There’s no reason why Smalltalk couldn’t be used to write theorem provers. It’s adept at machine learning, natural language processing, numerical computing, etc. Smalltalk is used heavily in academia, esp. in Europe and esp. at INRIA.
BTW, Smalltalk is great for robotics and Internet of Things, too.
If you’re interested in learning Smalltalk, I can recommend the beta release of “Updated Pharo by Example.” There’s also a terrific Pharo MOOC. Here’s a great blog. The late James Robertson has a fine series of instructional videos (he was a well-known Smalltalk evangelist). For people who need a really, really gentle introduction to Smalltalk, Prof Stef is nice.
I wrote this TechBeacon article on Smalltalk.