Comment by mccoyb
8 months 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.
8 months 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.
Yes, 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.