Proof Market: Submit Coq proof, get paid with Bitcoin
proofmarket.org
Proof Market: Submit Coq proof, get paid with Bitcoin
1–10 of 31 posts
Re: Proof Market: Submit Coq proof, get paid with Bitcoin
#2This sort of 'market' could surely be used for many other use-cases.
Re: Proof Market: Submit Coq proof, get paid with Bitcoin
#3Hm. Seems like it would make more sense for 'buyers' to submit btc along with the problem, which the market could then hold in escrow and release as soon as a proof passing the verifier was submitted. No need to trust anyone but the escrow service, between btc and machine proofs.
Re: Proof Market: Submit Coq proof, get paid with Bitcoin
#4I like the idea, however it appears as if the buyer has to wait until the seller has done the work before sending them payment.
How much confidence could the seller (i.e. the person doing the proof) have about the buyers ability to pay before they embark on completing the work?
A much better approach would be the buyer puts up the problem they want a proof for and then pays an escrow service, that way you can have more confidence that payment will be completed.
Re: Proof Market: Submit Coq proof, get paid with Bitcoin
#5This is a bit ordinary, since it is fundamentally just an escrow service.
What would be really cool is to find a way to "lock" the bitcoins so that only a correct proof in Coq of the given theorem could unlock them. Kind of like holomorphic encryption.
Re: Proof Market: Submit Coq proof, get paid with Bitcoin
#6This is a bit ordinary, since it is fundamentally just an escrow service. What would be really cool is to find a way to "lock" the bitcoins so that only a correct proof in Coq of the given theorem could unlock them. Kind of like holomorphic encryption.
You probably mean homomorphic encryption[1].
Re: Proof Market: Submit Coq proof, get paid with Bitcoin
#7This is a bit ordinary, since it is fundamentally just an escrow service. What would be really cool is to find a way to "lock" the bitcoins so that only a correct proof in Coq of the given theorem could unlock them. Kind of like holomorphic encryption.
Bitcoin does have a (non-turing-complete) scripting language built in for ensuring that transactions meet arbitrary requirements. I wonder what subset of proofs could be verified in that environment.
Re: Proof Market: Submit Coq proof, get paid with Bitcoin
#8Escrow implementation details aside, I love the idea of paying for information with a system that provides a method for communicating information securely between two parties. One of the more overlooked features of Bitcoin allows for message signing: http://bitcoin.stackexchange.com/questions/3337/what-are-the...
With a signing method, you can simultaneously prove someone created information containing a solution to a problem and the fact someone else paid them for the information.
Re: Proof Market: Submit Coq proof, get paid with Bitcoin
#9This sort of 'market' could surely be used for many other use-cases.
It actually can't -- a fundamental characteristic of this marketplace is that the work can be automatically verified [1].
As part of my PhD work, I created a service for crowdsourcing the verification of Java programs which relied on the same characteristic: http://homes.cs.washington.edu/~mernst/pubs/veriweb-oopsla20....
One limitation of these crowd-sourcing approaches is that, in practice, validation ("are we trying to build/prove the right thing?") is as important, if not more important, than verification.
[1] this might not be quite true yet, since a solution of "admitted." would pass the Coq checker.
Re: Proof Market: Submit Coq proof, get paid with Bitcoin
#10This sort of 'market' could surely be used for many other use-cases.
It actually can't -- a fundamental characteristic of this marketplace is that the work can be automatically verified [1]. As part of my PhD work, I created a service for crowdsourcing the verification of Java programs which relied on the same characteristic: http://homes.cs.washington.edu/~mernst/pubs/veriweb-oopsla20... . One limitation of these crowd-sourcing approaches is that, in practice, validation ("are we try…
Is that something a grep couldn't fix?