Using my definition of EVM, I think it's already possible to create a small verified compiler. My priority is on keeping the formal definition in sync with the Yellow Paper and the implementations.
There is a similar site [1] without external incentives (actually Proof Market is based on this). This site has active audience posting problems and proofs. Possibly Proof Market ends up in another example of…
This gives very broad perspective. I want to cite this comment when I talk about the site. I have never thought about disrupting Wall St, but I do share your pipe dream.
I added risks and complications. A feature called "bounty" is now available. Anyone can add bounty for a problem. The sum goes to the next solver.
I wonder which is easier to encode, natural deduction or Hilbert style.
"admit" does not pass the checker right now. coqchk -o is used to detect those assumptions.
I can mix both approaches. The buyer and other people can stash up bounty, which the first prover gets. I have not implemented this lest "bitcoin stolen from Coq proof exchange".
Using my definition of EVM, I think it's already possible to create a small verified compiler. My priority is on keeping the formal definition in sync with the Yellow Paper and the implementations.
There is a similar site [1] without external incentives (actually Proof Market is based on this). This site has active audience posting problems and proofs. Possibly Proof Market ends up in another example of…
This gives very broad perspective. I want to cite this comment when I talk about the site. I have never thought about disrupting Wall St, but I do share your pipe dream.
I added risks and complications. A feature called "bounty" is now available. Anyone can add bounty for a problem. The sum goes to the next solver.
I wonder which is easier to encode, natural deduction or Hilbert style.
"admit" does not pass the checker right now. coqchk -o is used to detect those assumptions.
I can mix both approaches. The buyer and other people can stash up bounty, which the first prover gets. I have not implemented this lest "bitcoin stolen from Coq proof exchange".