7 ms·
This is cool! Is the idea to put Kind2 on top of this in some way? I’d also love to find an example of writing a small interpreter in Bend - which runs on the
by mccoyb 2y ago
This is cool! Is the idea to put Kind2 on top of this in some way?
I’d also love to find an example of writing a small interpreter in Bend - which runs on the GPU.
- LightMachine 2y agoYes, Kind2 will be a type layer on top of Bend, with a similar relationship as in JavaScript / TypeScript (but much more integrated, less ad-hoc and with proofs!). I don't want Kind2 to compete directly with Lean though, as it is doing an amazing job and I'm rooting for it. So, Kind2 will be just a type system for Bend that happens to let you prove theorems about your programs, rather than a higher promise to digitalize all of maths and stuff.