[PRE-ANN] Qeditas: A Formal Library as a Bitcoin Spin-Off

[cryptic4000]

i dont understand anything.. but looks good 

lol. Maybe you should rephrase "I am ready with my BTC for gamble. Game is on."

[kushti]

Can you recommend any books / tutorial on Egal? Even with Coq (which is pretty popular) I have problems on regular basis with finding information able to help me in the internets. I'm not a mathematician

Do you have ETA for opensourcing Qeditas code in Ocaml?

[Bill White]

Can you recommend any books / tutorial on Egal? Even with Coq (which is pretty popular) I have problems on regular basis with finding information able to help me in the internets. I'm not a mathematician

As far as I know the only thing written about Egal is the manual: http://mathgate.info/egalmanual.pdf
It also comes with the source code: http://mathgate.info/egal.tgz

Without going into a review, the manual isn't very professionally written. Nevertheless, it was a valuable resource when I started trying to understand the code in December. I'm not sure the manual is good as a tutorial, but the first chapter does have some very simple examples.

Do you have ETA for opensourcing Qeditas code in Ocaml?

My intention has been to get a test version working before opensourcing it. This has taken longer than I expected. I will estimate mid-May, but it's only an estimate.

[Trent Russell]

Can you recommend any books / tutorial on Egal? Even with Coq (which is pretty popular) I have problems on regular basis with finding information able to help me in the internets. I'm not a mathematician

As far as I know the only thing written about Egal is the manual: http://mathgate.info/egalmanual.pdf
It also comes with the source code: http://mathgate.info/egal.tgz

Without going into a review, the manual isn't very professionally written. Nevertheless, it was a valuable resource when I started trying to understand the code in December. I'm not sure the manual is good as a tutorial, but the first chapter does have some very simple examples.

If someone wants to look at introductory examples, there are a lot of them in the documents from last year's treasure hunt.

https://mathgate.info/d/doc.php

Edit: Just looked at the manual. Looks like these documents are talked about in chapter 6.

[provenceday]

it's interesting.

will look this later.

[Bill White]

it's interesting.

will look this later.

Great!

If someone wants to look at introductory examples, there are a lot of them in the documents from last year's treasure hunt.

https://mathgate.info/d/doc.php

Edit: Just looked at the manual. Looks like these documents are talked about in chapter 6.

Thank you for posting this link. I should've thought of it yesterday.

[d-leit]

i will look at Egal, but i would still be more likely to try things out if it used Coq instead.

about selling claims you wrote this:

When your coin launches, it may trade at 0.01% of the bitcoin market cap.  You can buy 10,000 of your alt coins for 1 BTC.  If you continue to develop your alt, and if people begin to agree that it is useful, your 10,000 alt coins will be worth more than 1 BTC (possibly a lot more).

Since I am interested in the success of Qeditas, I would be willing to buy 10,000 (Qeditas) fraenks for 1 bitcoin when the network starts. I suppose a developer being forced to buy his own coin is a bit strange, but it's also part of why I like the idea. I hope it makes it clear to reasonable people that this is a project I'm doing because I believe in it.

and:

Address 1LvNDhCXmiWwQ3yeukjMLZYgW7HT9wCMru had a balance of 1.5 mbits at the time of the snapshot.

Suppose Alice is has the private key for this Bitcoin address.

Suppose Bob with the Qeditas address QVmqaNmBE3GbTPG3kqNh75mYpA6uUcxs35 wants to buy this claim from Alice.

Alice can sign a message

"endorse QVmqaNmBE3GbTPG3kqNh75mYpA6uUcxs35"

with her bitcoin address. Qeditas will use such a signed message to allow Bob to spend from the Qeditas address corresponding to 1LvNDhCXmiWwQ3yeukjMLZYgW7HT9wCMru.

Presumably Bob will pay some bitcoins to Alice's address above in exchange for this endorsement (although at an exchange rate of 10000:1, Bob would only need to pay Alice 15 satoshis).

Note that this will not require Alice to download or use Qeditas or any third party software.

Please post if you have any questions. Otherwise I will try to post updates as appropriate.

Do you still plan to use this "endorse" idea to buy people's claims? If so, you could begin buying these signed endorsements already (pre-lounch), right? i have two addresses that had about 0.4 bitcoins in them each, so i guess you're saying you would pay me 0.00008 for two signed endorsements messages? probably the fee isn't worth sending me 0.00008 bitcoins. It seems like practically you could only buy claims of people who have addresses with a lot of bitcoins.

[Bill White]

i will look at Egal, but i would still be more likely to try things out if it used Coq instead.

Now that I am modifying the plan to allow for generic theories/signatures, the choice of theorem prover is not so vital. Qeditas will probably use the type checking/proof checking code from Egal, but that's all. To publish a Qeditas document only the "compiled" document will be required and it should be easy to make modifications to a number of theorem provers to produce the kind of document Qeditas expects. It's conceivable that some users will produce the documents with a slightly modified version of Coq while others will produce them with a slightly modified version of Egal.

Do you still plan to use this "endorse" idea to buy people's claims? If so, you could begin buying these signed endorsements already (pre-lounch), right? i have two addresses that had about 0.4 bitcoins in them each, so i guess you're saying you would pay me 0.00008 for two signed endorsements messages? probably the fee isn't worth sending me 0.00008 bitcoins. It seems like practically you could only buy claims of people who have addresses with a lot of bitcoins.

Yes, I do still plan to buy people's claims as bitcoin-signed "endorsements." Maybe for small claims like the ones you are describing it makes sense to buy combine many of the bitcoin payments into one bitcoin transaction with many small outputs. I'll think about a way to do this.

[Bill White]

The Coq code corresponding to the theory of Qeditas has been updated to include theories and signatures:

git clone git://qeditas.org/qeditastheory.git

Allowing general theories will make Qeditas more flexible as it will be able to support different foundations. Signatures will allow people to more easily import common definitions and previous results into their documents.

In addition the part of the formalization dealing with the underlying logic is now more detailed (MathData.v).

My previous estimate for when the first ocaml code would be released was in mid-May, but it is likely I will need another week.

[Nthused]

So a bit like CLAM ?

[Bill White]

So a bit like CLAM ?

The initial Qeditas distribution is like CLAM in that it is based on a snapshot of the Bitcoin block chain. There are three differences: The initial distribution of Qeditas fraenks will be the same as the number of bitcoins at the corresponding address at the time of the snapshot. Secondly, Qeditas is only using the Bitcoin block chain, whereas CLAM also used Litecoin and Dogecoin. Finally, using endorsement messages it will be possible to sell Qeditas units without needing to download the Qeditas software or compromising the corresponding private keys.

[Bill White]

I created a fork of Egal to support Qeditas.

git clone git://qeditas.org/egal.git

github is warning me about my profile being hidden from the public for some reason. If github doesn't show it to you, you might still be able to clone it:

git clone https://github.com/billlwhite/egal.git

For the most part this fork is the same as the Egal released last year which can still be found here:

http://mathgate.info/egalrelease.php

(Incidentally, there are still 9 theorems in the file oldformaldocs/CategoryProblems.mg with bitcoin "treasures". I have been able to prove all the theorems and released my solutions as oldformaldocs/CategoryPartialSolns.mg, but in 9 cases I don't have a proof that gives the right private key.)

There's a minor difference in how polymorphic definitions are handled that makes this fork of Egal in some ways incompatible with the original Egal, but I included a new command line argument "-polyexpand" that replicates the old behavior.

The main thing that is new is the ability to create Qeditas theories, signatures and documents. Qeditas documents are in a binary format which is not intended to be created directly. Egal can be used to specify documents in an ASCII format that can be written and read by humans. This new fork of Egal can output the binary format Qeditas requires. To support this some of the code I've written for Qeditas was included in a subdirectory src/qeditas.

Several examples based on the mathgate documents can be found in qeditasdocs1 and qeditasdocs2.

Since there's interest in using Coq instead of Egal, someone familiar with Coq might be interested in doing something similar with Coq. I suspect the simplest method for creating Qeditas documents with Coq is to translate from compiled Coq files to Qeditas documents.

The code for Qeditas itself is still in production. I keep hoping I will have a preliminary version of Qeditas ready within a week. Hopefully this prediction will soon be correct.

[Bill White]

Just in case bitcointalk.org goes down for a significant amount of time again, I'll point out that I have the domain qeditas.org. Currently it's just a collection of Qeditas related links (e.g., a link to this thread), but I could make it the place for announcements if it becomes necessary.

[jamesjde]

I am unable to see any of the GitHub content (404).

[Trent Russell]

I am unable to see any of the GitHub content (404).

Same for me.

Edit: But cloning does seem to work. Strange.

Code:

git clone https://github.com/billlwhite/egal.git

[Bill White]

This is unpleasant news to wake up to, but thanks for informing me. I will look into alternatives to github.

[Bill White]

github has unhidden my profile, so the repositories should all be visible via the links again now. I may set up my own git server to remove this unnecessary dependence on a third party site (github).

Edit (June 26 2015): The git repos are now hosted at qeditas.org.

Code:

git clone git://qeditas.org/qeditas.git
git clone git://qeditas.org/qeditastheory.git
git clone git://qeditas.org/cryptohash.git
git clone git://qeditas.org/ledgertheory.git
git clone git://qeditas.org/egal.git

They can also be viewed using gitweb here:

qeditas.org/gitweb

[Trent Russell]

I've tried to compile your fork of Egal, but I can't even get started. I'm using Tails OS which doesn't have make. This means I can't compile using the usual configure, make, make install. (Tails OS doesn't have ocaml either, but I compiled ocaml for Tails earlier.) I could start Tails with the ability to sudo, install make, and then Egal might compile, but this is a time consuming process.

The original Egal included a bash script makebytecode that compiled the bytecode version without requiring make. I tried using this old script on your fork, but it doesn't work. First, the script expects there to be a bin directory, which is not in your Egal. This is easy enough to fix with mkdir bin. Then calling the script I got this:

Code:

365 states, 24874 transitions, table size 101686 bytes
File "src/mgcheck.ml", line 40, characters 0-23:
Error: Unbound module Axioms

At this point, I decided to give up and write this post. Can you include a script like the old makebytecode that can compile Egal without make?

[Bill White]

I've tried to compile your fork of Egal, but I can't even get started. I'm using Tails OS which doesn't have make. This means I can't compile using the usual configure, make, make install. (Tails OS doesn't have ocaml either, but I compiled ocaml for Tails earlier.) I could start Tails with the ability to sudo, install make, and then Egal might compile, but this is a time consuming process.

The original Egal included a bash script makebytecode that compiled the bytecode version without requiring make. I tried using this old script on your fork, but it doesn't work. First, the script expects there to be a bin directory, which is not in your Egal. This is easy enough to fix with mkdir bin. Then calling the script I got this:

Code:

365 states, 24874 transitions, table size 101686 bytes
File "src/mgcheck.ml", line 40, characters 0-23:
Error: Unbound module Axioms

At this point, I decided to give up and write this post. Can you include a script like the old makebytecode that can compile Egal without make?

Thank you for the feedback. I thought I had an empty bin directory in the repo, but I was wrong. This has been fixed. I also modified the old Egal's makebytecode script to work for the new Egal and added it. You should now be able to compile Egal using makebytecode as long as openssl, ocamllex and ocamlc are in your bash path.

[Trent Russell]

Thank you for the feedback. I thought I had an empty bin directory in the repo, but I was wrong. This has been fixed. I also modified the old Egal's makebytecode script to work for the new Egal and added it. You should now be able to compile Egal using makebytecode as long as openssl, ocamllex and ocamlc are in your bash path.

Just to confirm, the new makebytecode script does compile under Tails for me now.