A week or so ago I was browsing /r/Python and I saw a link to a website called rise4fun.com, which is a Microsoft Research project that contains a lot of cool demos and tools that you can run in your browser. The demo I was linked to was a restricted Python shell that could be used to experiment with a “high performance theorem prover” called Z3. Python is a highly dynamic language and so it is pr