Upgrade to Pro — share decks privately, control downloads, hide ads and more …

Programming Languages x Blockchains

Avatar for Volodymyr Kyrylov Volodymyr Kyrylov
April 25, 2018
Technology
1
240

Programming Languages x Blockchains

Are you sure you still want smart contracts? Presented on iForum 2018
Avatar for Volodymyr Kyrylov

Volodymyr Kyrylov

April 25, 2018
Tweet

More Decks by Volodymyr Kyrylov

See All by Volodymyr Kyrylov
Ur/Web: lightning fast prototyping for the web
Avatar for Volodymyr Kyrylov proger
0
250
Swift to Haskell: Overloading Semicolons
Avatar for Volodymyr Kyrylov proger
2
210
The Programming Language of Mathematics
Avatar for Volodymyr Kyrylov proger
3
670
Stochastic Relaxation, Gibbs Distributions, and the Bayesian Restoration of Images
Avatar for Volodymyr Kyrylov proger
0
1k
Monosyn - monocular navigation for robots
Avatar for Volodymyr Kyrylov proger
0
130
Lambda the Ultimate Devops v2
Avatar for Volodymyr Kyrylov proger
1
470
Lambda the Ultimate Devops
Avatar for Volodymyr Kyrylov proger
0
270
Haskell >>= DevOps
Avatar for Volodymyr Kyrylov proger
0
870
The Zalora Platform
Avatar for Volodymyr Kyrylov proger
2
850

Other Decks in Technology

See All in Technology
2025-04-24 "Manga AI Understanding & Localization" Furukawa Arata (CyberAgent, Inc)
Avatar for Arata Furukawa ornew
2
330
Perl歴約10年のエンジニアがフルスタックTypeScriptに出会ってみた
Avatar for papix papix
1
260
ここはMCPの夜明けまえ
Avatar for nwiizo nwiizo
32
13k
Gateway H2 モジュールで
スマートホーム入門
Avatar for MinoruInachi minoruinachi
0
120
Новые мапы в Go. Вова Марунин, Clatch, МТС
Avatar for Lamoda Tech lamodatech
0
1.6k
Goの組織でバックエンドTypeScriptを採用してどうだったか / How was adopting backend TypeScript in a Golang company
Avatar for 株式会社カミナシ kaminashi
12
9.1k
PagerDuty×ポストモーテムで築く障害対応文化/Building a culture of incident response with PagerDuty and postmortems
Avatar for AEON aeonpeople
3
540
ペアーズにおける評価ドリブンな AI Agent 開発のご紹介
Avatar for fukubaka0825 fukubaka0825
7
2k
「経験の点」の位置を意識したキャリア形成 / Career development with an awareness of the “point of experience” position
Avatar for Pauli pauli
4
130
OPENLOGI Company Profile for engineer
Avatar for OPENLOGI hr01
1
25k
Microsoft の SSE の現在地
Avatar for skmkzyk skmkzyk
0
280
Dynamic Reteaming And Self Organization
Avatar for Miho Nagase miholovesq
3
740

Featured

See All Featured
Art, The Web, and Tiny UX
Avatar for Lynn Fisher lynnandtonic
298
20k
Let's Do A Bunch of Simple Stuff to Make Websites Faster
Avatar for Chris Coyier chriscoyier
507
140k
No one is an island. Learnings from fostering a developers community.
Avatar for Antonio thoeni
21
3.3k
Into the Great Unknown - MozCon
Avatar for Noah Learner thekraken
38
1.7k
Cheating the UX When There Is Nothing More to Optimize - PixelPioneers
Avatar for Stéphanie Walter stephaniewalter
280
13k
Mobile First: as difficult as doing things right
Avatar for Swwweet swwweet
223
9.6k
RailsConf 2023
Avatar for Aaron Patterson tenderlove
30
1.1k
Performance Is Good for Brains [We Love Speed 2024]
Avatar for Tammy Everts tammyeverts
10
780
The World Runs on Bad Software
Avatar for Brandon Keepers bkeepers
PRO
68
11k
ピンチをチャンスに：未来をつくるプロダクトロードマップ #pmconf2020
Avatar for Aki / @LoveIdahoBurger aki_iinuma
119
51k
Build your cross-platform service in a week with App Engine
Avatar for Jose L jlugia
230
18k
Designing for Performance
Avatar for Lara Hogan lara
608
69k

Transcript

  1. Programming Languages × Blockchains Vlad Ki ESM.one

  2. Mainstream PLs won't work

  3. None

  4. DApps in 2013

  5. None
  6. None
  7. None
  8. None
  9. None

  10. DApps in 2018

  11. None

  12. 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; }

  13. #!/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

  14. WTF?!

  15. Developers are losing abstractions!

  16. ACID Atomic Consistent Isolated Durable

  17. BEGIN TRANSACTION ISOLATION LEVEL SERIALIZABLE; UPDATE accounts SET balance =

    balance + 100 WHERE addr = 0x4206f95fc533483; UPDATE accounts SET balance = balance - 100 WHERE addr = 0x083c41ea13af6c2; COMMIT;

  18. SELECT address FROM accounts ORDER BY random() LIMIT 1;

  19. 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;

  20. BASE Basically Available Soft State Eventually Consistent

  21. http:/ /docs.basho.com/riak/kv/2.2.3/learn/concepts/clusters/

  22. $ 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

  23. Logical Clocks https:/ /cacm.acm.org/magazines/2016/4/200168-why-logical-clocks-are-easy/abstract

  24. https:/ /hal.inria.fr/file/index/docid/555588/filename/techreport.pdf

  25. 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.

  26. $ 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}

  27. В риаке конфликты на чтение Пиши в блокчейн! А зачем?

    Глобальный консенсус! Так языка запросов даже нет! Ты чё, пёс, это же крипта!

  28. UTXO Unconvincing Transaction Outcome

  29. 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.

  30. european :: Date -> Contract -> Contract european t u

    = at t (u `or` zero)
  31. None

  32. 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.

  33. pragma solidity ^0.4.0; contract SimpleStorage { uint storedData; function set(uint

    x) public { storedData = x; } function get() public constant returns (uint) { return storedData; } }

  34. 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; }
  35. None

  36. 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" }

  37. Why?

  38. None
  39. None

  40. 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
  41. None
  42. None

  43. Ensure Properties!

  44. None

  45. Coq Dependent Type Theory Tactics Extraction to OCaml and Haskell

    Formalization of mathematics

  46. Theorem pred_and_succ_covariant: forall c: counter, pred (succ c) = succ

    (pred c). intros c. induction c. compute. reflexivity. Qed.
  47. None
  48. None

  49. 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; } }

  50. The DAO https:/ /abhiroop.github.io/Exceptions-and-Transactions/

  51. Interface State Machine Plutus Plutus Core Solidity EVM (stack) IELE

    (register) Chain Bitcoin Script Ivy Vyper
  52. None
  53. None

  54. Hardening Strategies Interfaces (*.h, *.mli) Interfaces + property claims (f

    . g = g . f) Interfaces + property proofs Implementation property claims Implementation property proofs

  55. Hardening Strategies End-to-end compilation Verify interfaces in Coq Use plutus

    core/iele as compilation targets

  56. Contracts as State Machines

  57. None

  58. Denotate to simple languages!

  59. None

  60. System F

  61. Turing vs Church

  62. Interface State Machine Plutus Plutus Core Solidity EVM (stack) IELE

    (register) Chain Bitcoin Script Ivy Vyper

  63. Interface State Machine Plutus Plutus Core Solidity EVM (stack) IELE

    (register) Chain Bitcoin Script Ivy Vyper run . compile = meaning

  64. Gotcha

  65. 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)

  66. 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.

  67. twitter.com/kievfprog kievfprog.net

  68. Haskell Rust Scala F# F* Ur Agda Idris Coq SML

    OCaml QuickCheck SMT
  69. None

  70. Yay Formal Methods! [email protected]