What solver would you have them use? Z3 is very mature and the Rust bindings are pretty good in my (limited) experience.
I would write the tutorial in C++, for a more direct experience.
alt Hacker News
I would write the tutorial in C++, for a more direct experience.