pirapira

31 ms·

1. 1.▲
   by pirapira 10y ago

   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.
2. 2.▲
   by pirapira 13y ago

   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 overjustification. [1] http:&
3. 3.▲
   by pirapira 13y ago

   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.
4. 4.▲
   by pirapira 13y ago

   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.
5. 5.▲
   by pirapira 13y ago

   I wonder which is easier to encode, natural deduction or Hilbert style.
6. 6.▲
   by pirapira 13y ago

   "admit" does not pass the checker right now. coqchk -o is used to detect those assumptions.
7. 7.▲
   by pirapira 13y ago

   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".