TLA+ for the design of BitCoin | Bitcointalksearch.org

jungly

newbie

Activity: 10

Merit: 5

Started work on specifying layer two bitcoin contracts using TLA+. The first goal is of course LN. However, writing LN contracts first requires specifying a bitcoin transactions module.

Repo: https://github.com/pool2win/bitcoin-contracts-tlaplus
BitcoinTransactions module: https://github.com/pool2win/bitcoin-contracts-tlaplus/blob/main/BitcoinTransactions.pdf
LNContracts module (soon to start using BitcoinTransactions module): https://github.com/pool2win/bitcoin-contracts-tlaplus/blob/main/LNContracts.pdf

I'll keep you posted on the progress. We already have the commitment transactions speced and next step is to spec the HTLC outputs in the commitment transactions.

Quote from: Gyrsur on August 13, 2018, 04:59:54 PM

I recently learned about TLA+ and are asking myself if Satoshi used this for the design of concurrent and distributed systems like BitCoin?

http://lamport.azurewebsites.net/tla/tla.html

http://lamport.azurewebsites.net/tla/hyperbook.html

http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-spec-tla-plus.pdf

Gyrsur

legendary

Activity: 2856

Merit: 1518

Bitcoin Legal Tender Countries: 2 of 206

Quote from: TheArchaeologist on August 14, 2018, 03:30:29 PM

Still looking for proof Leslie Lamport is Satoshi? Wink

there will be no proof ever in the future!

if true why should he proof it? which advantages will be the result? not a single advantage just many disadvantages.

LL is not in the position of CSW with Australian Taxation Office hunting him.

and he is the inventor of many other things he don't need the BitCoin inventor fame on top of the other things.

what maybe is possible that after his life time the truth about the inventor of BitCoin will be come to the light. maybe he will prepare something that should be revealed after he is not alive anymore.

watch nakamotofamilyfoundation.org. it could be the key to it.

Paxos Agreement - Computerphile

EDIT: http://nakamotofamilyfoundation.org/ is broken. where will the book have been published? Roll Eyes