Re:Kind: A Modern Proof Language
by rejectedandsad on Wednesday August 11, 2021 @09:55AM
(#28142004)
This is much cooler than I thought it would be and calling it a proof language seems to undersell it. It seems to be more of a general purpose FP language that can compile to multiple backends and supports UI development out of the box (!!)
[ Parent
| on HN ]
Any chance of supporting python? I have similar plans with py2many and http://adsharma.github.io/pysmt
Re:Kind: A Modern Proof Language
by LangMakers on Wednesday August 11, 2021 @11:08AM
(#28142931)
Yes! We're 1 file away from supporting a Python (and any other) back-end. For example, [this](https://github.com/uwu-tech/Kind/blob/master/base/Kind/Comp/...) is the simplified JS back-end. If you just copy/paste that file and edit the syntax to Python instead, we'll have a Python back-end. That kind of contribution is always welcome.
Love the ideas! I'm coming at it from the other side - I worked on a transpiler that targets 7+ languages already.
Also started with python, to avoid javascript warts that typescript carries forward for compatibility reasons. But hey, it's the most popular programming language out there - so you'll see plenty of people wanting to write code this way.
The higher order bit is that we both want to bring transpilation after proof tech to mainstream languages.