I implemented Prolog and Z3 as a function tool for my little OpenAI Assistants API client. Z3 (SMT-LIB, actually) seemed even more promising. The model speaks both languages. However, I didn't find any convincing use-cases yet. But it seems a logical extension of the idea to provide a programming language via a function tool to solve problems. So you start thinking "What else has text input and output, and a powerful engine in between?"