Smart Contract Verification
Tezos Japan, DaiLambda, Inc.
Jun FURUSE/古瀬 淳
Bit of myself: Past
OCaml researcher and programmer
- Studied type system of FP
- Like Haskell too
FP in Financial Systems
- Derivative modeling
- HFT(High Frequency Trading) systems
Bit of myself: Now
NPO to promote Tezos technology in Japan.
A small company to participate Tezos core development.
Bit of Tezos
- 3rd gen. cryptocurrency
(1st: Bitcoin, 2nd: Ethereum, 3rd: many)
- Consensus algorithm: Proof of Stake
- On Chain Governance
- Symbol ꜩ
- Written in OCaml
- Formal verification
- Brief History of Currency
- What is Blockchain?
- Technical Aspects of Blockchain
- Proof of Stake
- Bit more about Tezos
- Blockchain and Formal Verification
Brief History of Currency
Brief History of Currency
Main theme: “How to trade smoothly?”
👨 🌾 ← 🐟 👩
Birth of Currency
👨 🌾 ⇄ 🐚 ⇄ 🐟 👩
China, 1100 BC
Shell has a built-in value (beauty).
Conditions for Currencies
Scale of value (comparison of values)
Means of exchange (easy to carry)
Means of store of value (never rotten)
Mintable: Governments can control the money supply.
China, 800 BC (刀貨, 布貨)
- Coins have built-in values as precious metal.
- Seigniorage vs counterfait
Convertible Paper Money
Easier to carry
- Assured conversion to gold (or silver, copper)
- Total supply is limited to the government’s gold stock
- The medium of the currency has no built-in value.
→ More strict anti-counterfait requirements
The First Convertible Paper Money
交子 in China, around 1050
- Started as private notes for iron coins.
- 宋 dynasty assured the conversion between copper coins.
This is not currency, but optimized trade efficiency
by recording credit/debt using numbers.
Since 1971, at the end of Bretton Woods Agreements.
- No more support by precious metal, but money stayed as money.
- Confusions led to floating exchange rate system.
- Governments can control their money supply.
- Economy has boosted with more liquidity of currencies.
The First Fiat Money
交子 in China, around 1050, again.
- The world first convertible paper money
- … and soon became the world first fiat 😅
- … and lost its value since too many were printed.
No more medium. Just numbers in electrons.
- Pegged with government currencies.
- Very centralized. Manager companies are responsible for conversion.
- Cryptography to prevent forgery and cheating.
The Basis of the Value of Currencies
Less and less:
- The value of the medium: Nothing
- Convertible with precious metal: No
- The physical form as fiat: No
What Makes Money as Money?
- Means of paying tax
- You have to pay tax or you get arrested.
Radical Theory: Common Knowledge
Common knowledge that it is money.
With it, no need of centralized power!!
- Iraqi Swiss dinar (1993-2003)
- Somali shillings (1990’s)
Rise of Cryptocurrencies
Since 2009-01-03 (Bitcoin):
- Decentralized: no central bank
- Cryptography to prevent counterfait and cheating
Tracking vs Privacy
Electronic money made tracking much easier.
- Powers love tracking.
- Public do not like being tracked.
Nowadays, anonymity is another important condition of currencies.