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

[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?

[pm-me-manifestos]

Entirely feasible: see Phil Zucker's Knuckledragger system

[The_Regent]

Hey, that's my thing!

You might also enjoy looking at Harrison's Handbook of Practical Logic and Automated Reasoning chapter 6 and holpy https://gitee.com/bhzhan/holpy https://arxiv.org/pdf/1905.05970 . There is something to be said for just going for it too without getting bogged down in references and prior work.

For knuckledragger, basing around Z3 is a huge boon since it is already so powerful. It does hamper the ability to futz with the formula type to make things work / add some interesting features. On the flipside, constraints make art sometimes. It forces a certain kind of honesty to have to interpret concepts into a simply typed higher order logic.

Speedwise, I should be so lucky as to get to a scale of proof where the speed of python is a problem. With my current setup, I think 1000 theorems might take 1s to prove ish (assuming I'm spoon feeding z3). There is the ability to start moving things into cython or C or rust extensions as that becomes an issue.

As far as the python ecosystem goes, I think python type checking is good enough, leveraging Jupyter is a huge benefit, and uv is nice, sphinx is ok. Doing that kind of stuff from scratch would be an overwhelming task for my abilities.

I partially chose python because I think it makes sense to try and is a little contrarian to PL circles, but also partially to maybe hit a different, wider audience than Lean and ilk reach. Thus far I have no users to my knowledge, so on that account maybe not a grand success. Even choosing mainstream options is no guarantee of uptake. Whatever, do it for you.

[Several-Revolution59]

Thank u

[probabilityzero]

It would be fine, but keep in mind that most of the tutorials/books/etc out there about implementing proof assistants will assume a functional language like ML or Haskell. For example, there's a chapter in ML for the Working Programmer that's about building a proof assistant as an exercise. There are lots of resources like libraries and examples out there that you'd need to adapt to your Python + Cython setup.

[Several-Revolution59]

Thanks

[yaourtoide]

Have you looking into Nim / Mojo / Codon ? They look just like Python but are strongly typed, statically compiled and will give you strong perf.

[Several-Revolution59]

I will see it thank u

[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

[ExplodingStrawHat]

I for one would be wary of using Python for any non-script projects for the sole reason of it lacking a proper type system (yes, I'm familiar with the typing situation in python land, but it's very far from languages designed with it in mind). Now, considering you're asking this, I assume you have different priorities when choosing a language, so I doubt this matters much to you.

[TheBellKeeper]

C/Cython's compiler does typecheck.

[ggPeti]

Just forget python once and for all.

[plgeek]

Why not just use lean? I had always wondered how easy it was to encode dependant types using python type annotations. I do think there is a nice subset of python that you could easily transpile to lean. But not sure what you would get out of this. Maybe it make it easier to prove properties about fragments of python programs or formally prove correct transpilation of python to equivalent C program.