No, because we don’t emit a runtime for proofs, we...

# arrow

[raulraja]

No, because we don’t emit a runtime for proofs, we proof the runtime is correct based on axioms, the issue with agda is that you need to know agda and the runtime may not be what you want but this is generalized to mainstreams lang in their own syntax