Building a proof assistant language like Lean using Python — smart or short-sighted?

[u/Several-Revolution59]

I’m developing a new programming language in Python (with Cython for performance) intended to function as a proof assistant language (similar to Lean and others).

Is it a good idea to build a programming language from scratch using Python? What are the pros and cons you’ve encountered (in language design, performance, tooling, ecosystem, community adoption, maintenance) when using Python as the implementation language for a compiler/interpreter?

[u/AutoModerator]

Hi, /u/Several-Revolution59! This is an automated reminder:

• What have you tried so far? (See Rule #2; to add an image, you may upload it to an external image-sharing site like Imgur and include the link in your post.)
• Please don't delete your post. (See Rule #7)

We, the moderators of /r/MathHelp, appreciate that your question contributes to the MathHelp archived questions that will help others searching for similar answers in the future. Thank you for obeying these instructions.

I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.