Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
Programming Languages x Blockchains
Search
Volodymyr Kyrylov
April 25, 2018
Technology
1
250
Programming Languages x Blockchains
Are you sure you still want smart contracts? Presented on iForum 2018
Volodymyr Kyrylov
April 25, 2018
Tweet
Share
More Decks by Volodymyr Kyrylov
See All by Volodymyr Kyrylov
Ur/Web: lightning fast prototyping for the web
proger
0
250
Swift to Haskell: Overloading Semicolons
proger
2
230
The Programming Language of Mathematics
proger
3
680
Stochastic Relaxation, Gibbs Distributions, and the Bayesian Restoration of Images
proger
0
1.1k
Monosyn - monocular navigation for robots
proger
0
140
Lambda the Ultimate Devops v2
proger
1
480
Lambda the Ultimate Devops
proger
0
280
Haskell >>= DevOps
proger
0
900
The Zalora Platform
proger
2
860
Other Decks in Technology
See All in Technology
Claude Codeは仕様駆動の夢を見ない
gotalab555
0
130
大規模イベントに向けた ABEMA アーキテクチャの遍歴 ~ Platform Strategy 詳細解説 ~
nagapad
0
190
マルチプロダクト×マルチテナントを支えるモジュラモノリスを中心としたアソビューのアーキテクチャ
disc99
0
260
AWS re:Inforce 2025 re:Cap Update Pickup & AWS Control Tower の運用における考慮ポイント
htan
1
200
Perlアプリケーションで トレースを実装するまでの 工夫と苦労話
masayoshi
1
410
マルチモーダル基盤モデルに基づく動画と音の解析技術
lycorptech_jp
PRO
4
500
Tableau API連携の罠!?脱スプシを夢見たはずが、逆に依存を深めた話
cuebic9bic
3
210
専門分化が進む分業下でもユーザーが本当に欲しかったものを追求するプロダクトマネジメント/Focus on real user needs despite deep specialization and division of labor
moriyuya
0
970
Mambaで物体検出 完全に理解した
shirarei24
2
210
【2025 Japan AWS Jr. Champions Ignition】点から線、線から面へ〜僕たちが起こすコラボレーション・ムーブメント〜
amixedcolor
1
120
【CEDEC2025】ブランド力アップのためのコンテンツマーケティング~ゲーム会社における情報資産の活かし方~
cygames
PRO
0
230
私とAWSとの関わりの歩み~意志あるところに道は開けるかも?~
nagisa53
1
160
Featured
See All Featured
Automating Front-end Workflow
addyosmani
1370
200k
Being A Developer After 40
akosma
90
590k
The Cost Of JavaScript in 2023
addyosmani
51
8.7k
Performance Is Good for Brains [We Love Speed 2024]
tammyeverts
10
1k
Speed Design
sergeychernyshev
32
1.1k
Rebuilding a faster, lazier Slack
samanthasiow
83
9.1k
Imperfection Machines: The Place of Print at Facebook
scottboms
267
13k
Site-Speed That Sticks
csswizardry
10
750
Testing 201, or: Great Expectations
jmmastey
45
7.6k
The Psychology of Web Performance [Beyond Tellerrand 2023]
tammyeverts
48
2.9k
The Power of CSS Pseudo Elements
geoffreycrofte
77
5.9k
The Pragmatic Product Professional
lauravandoore
36
6.8k
Transcript
Programming Languages × Blockchains Vlad Ki ESM.one
Mainstream PLs won't work
None
DApps in 2013
None
None
None
None
None
DApps in 2018
None
function createGen0Auction(uint256 _genes) public onlyCOO { require(gen0CreatedCount < gen0CreationLimit); uint256
kittyId = _createKitty(0, 0, 0, _genes, address(this)); _approve(kittyId, saleAuction); saleAuction.createAuction(kittyId, _computeNextGen0Price(), 0, gen0AuctionDuration, address(this)); gen0CreatedCount++; } function _computeNextGen0Price() internal view returns (uint256) { uint256 avePrice = saleAuction.averageGen0SalePrice(); require(avePrice < 340282366920938463463374607431768211455); uint256 nextPrice = avePrice + (avePrice / 2); if (nextPrice < gen0StartingPrice) { nextPrice = gen0StartingPrice; } return nextPrice; }
#!/bin/bash while { echo -ne "HTTP/1.1 200 OK\r\nConnection: close\r\n\r\n<html>lol</ html>\r\n";
} \ | nc -l 80 do : done
WTF?!
Developers are losing abstractions!
ACID Atomic Consistent Isolated Durable
BEGIN TRANSACTION ISOLATION LEVEL SERIALIZABLE; UPDATE accounts SET balance =
balance + 100 WHERE addr = 0x4206f95fc533483; UPDATE accounts SET balance = balance - 100 WHERE addr = 0x083c41ea13af6c2; COMMIT;
SELECT address FROM accounts ORDER BY random() LIMIT 1;
CREATE SEQUENCE txn; BEGIN TRANSACTION ISOLATION LEVEL SERIALIZABLE; INSERT INTO
tx VALUES (nextval('txn'), current_timestamp); INSERT INTO tx VALUES (nextval('txn'), current_timestamp); COMMIT;
BASE Basically Available Soft State Eventually Consistent
http:/ /docs.basho.com/riak/kv/2.2.3/learn/concepts/clusters/
$ curl http://riak/buckets/chain/keys/0x4206f95fc533483 < HTTP/1.1 300 Multiple Choices < X-Riak-Vclock:
a85hYGDgyGDKBVIszMk55zKYEhnzWBlKIniO8kGF2TyvHYIKf0cIszUnMTBz HYVKbIhEUl+VK4spDFTPxhHzFyqhEoVQz7wkSAGLMGuz6FSocFIUijE3pt5H lsgCAA== < Content-Type: multipart/mixed; boundary=lol --lol Content-Type: application/json Link: </buckets/chain>; rel="up" Etag: 16vic4eU9ny46o4KPiDz1f Last-Modified: Wed, 10 Mar 2010 18:01:06 GMT 100 --lol Content-Type: application/json Link: </buckets/chain>; rel="up" Etag: 4v5xOg4bVwUYZdMkqf0d6I Last-Modified: Wed, 10 Mar 2010 18:00:04 GMT 200
Logical Clocks https:/ /cacm.acm.org/magazines/2016/4/200168-why-logical-clocks-are-easy/abstract
https:/ /hal.inria.fr/file/index/docid/555588/filename/techreport.pdf
Definition counter : Type := nat * nat. Definition zero
:= (O, O). Definition succ (c : counter) := match c with (p, n) => (p + 1, n) end. Definition pred (c : counter) := match c with (p, n) => (p, n + 1) end.
$ curl -XPOST http://riak/types/counters/buckets/ chain/datatypes/0x4206f95fc533483 \ -d '{"increment": 100}' $
curl -XPOST http://riak/types/counters/buckets/ chain/datatypes/0x4206f95fc533483 \ -d '{"decrement": 50}' $ curl http://riak/types/counters/buckets/chain/ datatypes/0x4206f95fc533483 {"type":"counter", "value": 100}
В риаке конфликты на чтение Пиши в блокчейн! А зачем?
Глобальный консенсус! Так языка запросов даже нет! Ты чё, пёс, это же крипта!
UTXO Unconvincing Transaction Outcome
Smart Contracts Smart contracts help you exchange money, property, shares,
or anything of value in a transparent, conflict-free way while avoiding the services of a middleman.
european :: Date -> Contract -> Contract european t u
= at t (u `or` zero)
None
Smart Contracts Smart contracts are executable programs run on top
of an immutable distributed database whose inputs and outputs are maintained globally consistent by a distributed consensus protocol.
pragma solidity ^0.4.0; contract SimpleStorage { uint storedData; function set(uint
x) public { storedData = x; } function get() public constant returns (uint) { return storedData; } }
function createGen0Auction(uint256 _genes) public onlyCOO { require(gen0CreatedCount < gen0CreationLimit); uint256
kittyId = _createKitty(0, 0, 0, _genes, address(this)); _approve(kittyId, saleAuction); saleAuction.createAuction(kittyId, _computeNextGen0Price(), 0, gen0AuctionDuration, address(this)); gen0CreatedCount++; } function _computeNextGen0Price() internal view returns (uint256) { uint256 avePrice = saleAuction.averageGen0SalePrice(); require(avePrice < 340282366920938463463374607431768211455); uint256 nextPrice = avePrice + (avePrice / 2); if (nextPrice < gen0StartingPrice) { nextPrice = gen0StartingPrice; } return nextPrice; }
None
web3.eth.getTransaction('0x9fc76417374aa880d4449a1f7f31ec5 97f00b1f6f3dd2d66f4c9c6c445836d8b§234') .then(console.log); > { "hash": "0x9fc76417374aa880d4449a1f7f31ec597f00b1f6f3dd2d66f4c9c6c 445836d8b", "nonce": 2,
"blockHash": "0xef95f2f1ed3ca60b048b4bf67cde2195961e0bba6f70bcbea9a2c4e 133e34b46", "blockNumber": 3, "transactionIndex": 0, "from": "0xa94f5374fce5edbc8e2a8697c15331677e6ebf0b", "to": "0x6295ee1b4f6dd65047762f924ecd367c17eabf8f", "value": '123450000000000000', "gas": 314159, "gasPrice": '2000000000000', "input": "0x57cb2fc4" }
Why?
None
None
ERC20 allowance contract ERC20 is ERC20Basic { function transferFrom(address from,
address to, uint256 value) public returns (bool); function approve(address spender, uint256 value) public returns (bool); } https:/ /docs.google.com/document/d/ 1YLPtQxZu1UAvO9cZ1O2RPXBbT0mooh4DYKjA_jp-RLM/edit https:/ /github.com/ethereum/EIPs/blob/master/EIPS/eip-20.md
None
None
Ensure Properties!
None
Coq Dependent Type Theory Tactics Extraction to OCaml and Haskell
Formalization of mathematics
Theorem pred_and_succ_covariant: forall c: counter, pred (succ c) = succ
(pred c). intros c. induction c. compute. reflexivity. Qed.
None
None
pragma solidity ^0.4.0; contract Fund { mapping(address => uint) shares;
function withdraw() public { if (msg.sender.call.value(shares[msg.sender])()) shares[msg.sender] = 0; } }
The DAO https:/ /abhiroop.github.io/Exceptions-and-Transactions/
Interface State Machine Plutus Plutus Core Solidity EVM (stack) IELE
(register) Chain Bitcoin Script Ivy Vyper
None
None
Hardening Strategies Interfaces (*.h, *.mli) Interfaces + property claims (f
. g = g . f) Interfaces + property proofs Implementation property claims Implementation property proofs
Hardening Strategies End-to-end compilation Verify interfaces in Coq Use plutus
core/iele as compilation targets
Contracts as State Machines
None
Denotate to simple languages!
None
System F
Turing vs Church
Interface State Machine Plutus Plutus Core Solidity EVM (stack) IELE
(register) Chain Bitcoin Script Ivy Vyper
Interface State Machine Plutus Plutus Core Solidity EVM (stack) IELE
(register) Chain Bitcoin Script Ivy Vyper run . compile = meaning
Gotcha
gcd :: (Integral a) => a -> a -> a
gcd x y = gcd' (abs x) (abs y) where gcd' a 0 = a gcd' a b = gcd' b (a `rem` b)
Lemma euclid_rec : forall v3 : Z, (0 <= v3)%Z
-> forall u1 u2 u3 v1 v2 : Z, (u1 * a + u2 * b)%Z = u3 -> (v1 * a + v2 * b)%Z = v3 -> (forall d : Z, gcd u3 v3 d -> gcd a b d) -> Euclid. Proof. intros v3 Hv3; generalize Hv3; pattern v3 in |- *. apply Z_lt_rec. clear v3 Hv3; intros. elim (Z_zerop x); intro. apply Euclid_intro with (u := u1) (v := u2) (d := u3). assumption. apply H2. rewrite a0; auto. set (q := (u3 / x)%Z) in *. assert (Hq : (0 <= u3 - q * x < x)%Z). replace (u3 - q * x)%Z with (u3 mod x)%Z. apply Z_mod_lt; omega. assert (xpos : (x > 0)%Z). omega. generalize (Z_div_mod_eq u3 x xpos). unfold q in |- *. intro eq; pattern u3 at 2 in |- *; rewrite eq; ring. apply (H (u3 - q * x)%Z Hq (proj1 Hq) v1 v2 x (u1 - q * v1)%Z (u2 - q * v2)%Z). tauto. replace ((u1 - q * v1) * a + (u2 - q * v2) * b)%Z with (u1 * a + u2 * b - q * (v1 * a + v2 * b))%Z. rewrite H0; rewrite H1; trivial. ring. intros; apply H2. apply gcd_for_euclid with q; assumption. assumption. Qed.
twitter.com/kievfprog kievfprog.net
Haskell Rust Scala F# F* Ur Agda Idris Coq SML
OCaml QuickCheck SMT
None
Yay Formal Methods!
[email protected]