Comment by stschaef
8 hours ago
After looking through things a little more, I think I may have had some misunderstandings. Would you be willing to answer a few more questions? I will also take a closer look at the papers at some point, so apologies if these are redundant
1. When I see a comparison of a new proof checker to something like Agda/Lean, I initially evaluate them as systems for formalized mathematics, but I don't think you're making claims of that nature. Would you say that you'd expect, say, the new giganto proof of Fermat's Last Theorem to be expressible in Bend and faster than the corresponding Lean proof?
2. If the answer to the last one is no, that's not expressible, then what is the class of propositions/types that you express? My initial reading was that it was the whole of affine dependent type theory
3. Is the GPU used at both runtime and compile time?
1. I do, but probably not in the current version, since I believe these proofs probably need full closure cloning to be ergonomic.
2. You can express anything actually, because you can clone data, just not functions. So, anything you could implement with datatypes (i.e., without cloned closures), you could probably also prove. But again, people use and abuse closure cloning a lot in Lean. So, how ergonomic would that be? I don't know. It is less about expressivity and more about ergonomics.
3. No, just in the runtime for now. Checking proofs on the GPU will happen when we implement Bend in itself.