0
$\begingroup$

I read that there are performance bottlenecks for proof assistants, and

verification of software often has 10x--100x as many lines of proof as lines of code being verified.

I guess there is also much run-time overhead for proof assistants compared to a program without proofs. I was just wondering if one can verify a piece of code and then generate this code in another language (e.g. python) that is more efficient to execute. In particular, I am interested in Lean 4 to generate scientific computing code in python.

Naively, I can think of using Lean to directly write python programs as strings. But just as using splitOn to parse CSV's. All sorts of things could go wrong.

So my general questions are:

Is there a well-established way to generate programs in another language in proof assistants?

Has any work been done in generating python code from Lean 4?

Improve this question
$\endgroup$
5
  • 2
    $\begingroup$ First question: yes, Lean can be extracted to C (or maybe C++?) and Coq can be extracted to a number of functional languages. However, extracting to Python? I’ve never seen anything making verified Python programs. Also I think for many applications, compiled Lean would be faster than Python. Although some native python string functions (as well as Numpy and Pandas) are quite fast (since they are written in C and very optimized). $\endgroup$ Commented Nov 25 at 11:42
  • 2
    $\begingroup$ Also the efficiency issues you mention (extra code for the proofs, etc), seem to be more issues about developer time and not about code execution time. $\endgroup$ Commented Nov 25 at 11:47
  • $\begingroup$ Is this question different from proofassistants.stackexchange.com/questions/5288/…? $\endgroup$ Commented Nov 26 at 16:43
  • $\begingroup$ @JeanAbouSamra. Yes, it is a different question. In the linked question, I asked whether one can call pip installed packages directly from Lean. From the comments therein, it is not very practical as of now. So, failing that, this question asks about one can generate python programs, and then hand it to a python interpreter. $\endgroup$ Commented 2 days ago
  • $\begingroup$ @JasonRute I am not 100% sure or know of an minimal example. But I think the extra code for proofs can take extra time. The proofs about the program are certainly useful. But as you said in the other question, we sometimes avoid over-use of type-class inferences to avoid making lean slow. $\endgroup$ Commented 2 days ago

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.