Bitcoin Forum

I recently learned about TLA+ (https://en.wikipedia.org/wiki/TLA%2B) 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

Still looking for proof Leslie Lamport is Satoshi? ;)

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 (https://youtu.be/s8JqcZtvnsM)

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

https://i.imgur.com/QohhDUX.png

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.