Author

Topic: TLA+ for the design of BitCoin (Read 252 times)

newbie
Activity: 10
Merit: 5
October 13, 2023, 05:57:34 AM
#4
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.

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
legendary
Activity: 2856
Merit: 1520
Bitcoin Legal Tender Countries: 2 of 206
August 15, 2018, 04:46:58 AM
#3
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

sr. member
Activity: 310
Merit: 727
---------> 1231006505
August 14, 2018, 02:30:29 PM
#2
Still looking for proof Leslie Lamport is Satoshi? Wink
legendary
Activity: 2856
Merit: 1520
Bitcoin Legal Tender Countries: 2 of 206
August 13, 2018, 03:59:54 PM
#1
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
Jump to: