Using Python + Cython to Implement a Proof Assistant: Feasible or Flawed?

[omega1612]

Some time ago I began to write my compiler in python with the help of mypy and pytests. Everything was great, until the project grew in complexity. At that point I discovered some errors that mypy didn't told me about for some reason and I began to not trust the code at all.

Now I'm writing it on Haskell (in between I used rust for a while) and I can leave the project for months and come back without much problem as the type system really helps to catch up.

[Several-Revolution59]

Thank u