3 ms·

I suspect that a Python DSL on top of Lean4 would be hugely popular, similar to PyTorch replacing existing Torch, which was written in Lua.

by ipsum2 3y ago

wslh 3y ago
... also like using Z3 with Python [1]. [1] https://ericpony.github.io/z3py-tutorial/guide-examples.htm https://ericpony.github.io/z3py-tutorial/guide-examples.htm
- ipsum2 3y ago
  This is quite nice! I wasn't aware of this.
epgui 3y ago
I have a very negative visceral reaction at the thought. (I am someone who uses python for work, and not for fun…)
- deleted 3y ago
  [deleted]
staunton 3y ago
Why do you suspect that? (Or was it ironic?)
rtpg 3y ago
I think the biggest jump between interactive theorem provers like Lean "normal" languages is the "interactive" part: Lean or Coq or the like really work well in a specialized IDE mode where you're editing the file and getting instant feedback about the state of your proof. You might be able to get a Python DSL to work, but there would be a lot of tooling work involved to pipe everything back. You can write proofs in a non-interactive way, but you're signing yourself up for a lot of tedium. EDIT: A video showing someone working through some simple stuff. You can obviously do a lot of things "in your head" but having the feedback loop is helpful. Though thinking about it more I don't think this precludes a Python DSL entirely. It would just require some smart design to support this form of interactivity. https://www.youtube.com/watch?v=VYFTph2izIs https://www.youtube.com/watch?v=VYFTph2izIs
Yoric 3y ago
That sounds... contradictory, isn't it? Python is immensely hostile to static analysis (note that I write this as someone who writes Python for a living, using pyright/mypy). If you remove the ability to perform static analysis from Lean, what's left? Or do you mean a Python-like syntax on top of Lean4? Note: Pretty sure that libtorch is written in C++ and CUDA.

I suspect that a Python DSL on top of Lean4 would be hugely popular, similar to PyTorch replacing existing Torch, which was written in Lua.

by ipsum2 3y ago

I suspect that a Python DSL on top of Lean4 would be hugely popular, similar to PyTorch replacing existing Torch, which was written in Lua.

wslh 3y ago

... also like using Z3 with Python [1]. [1] https://ericpony.github.io/z3py-tutorial/guide-examples.htm https://ericpony.github.io/z3py-tutorial/guide-examples.htm

ipsum2 3y ago
This is quite nice! I wasn't aware of this.

epgui 3y ago

I have a very negative visceral reaction at the thought. (I am someone who uses python for work, and not for fun…)

deleted 3y ago
[deleted]

staunton 3y ago

Why do you suspect that? (Or was it ironic?)

rtpg 3y ago

I think the biggest jump between interactive theorem provers like Lean "normal" languages is the "interactive" part: Lean or Coq or the like really work well in a specialized IDE mode where you're editing the file and getting instant feedback about the state of your proof. You might be able to get a Python DSL to work, but there would be a lot of tooling work involved to pipe everything back. You can write proofs in a non-interactive way, but you're signing yourself up for a lot of tedium. EDIT: A video showing someone working through some simple stuff. You can obviously do a lot of things "in your head" but having the feedback loop is helpful. Though thinking about it more I don't think this precludes a Python DSL entirely. It would just require some smart design to support this form of interactivity. https://www.youtube.com/watch?v=VYFTph2izIs https://www.youtube.com/watch?v=VYFTph2izIs

Yoric 3y ago

That sounds... contradictory, isn't it? Python is immensely hostile to static analysis (note that I write this as someone who writes Python for a living, using pyright/mypy). If you remove the ability to perform static analysis from Lean, what's left? Or do you mean a Python-like syntax on top of Lean4? Note: Pretty sure that libtorch is written in C++ and CUDA.