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
220
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
880
The Zalora Platform
Avatar for Volodymyr Kyrylov proger
2
850

Other Decks in Technology

See All in Technology
Digitization部 紹介資料
Avatar for Sansan, Inc. sansan33
PRO
1
3.8k
Scale Security Programs with Scorecarding
Avatar for Rami McCarthy ramimac
0
430
FastMCPでSQLをチェックしてくれるMCPサーバーを自作してCursorから動かしてみた
Avatar for Nayuta S. nayuts
1
210
AIに実況させる / AI Streamer
Avatar for motemen motemen
3
1.4k
データ戦略部門 紹介資料
Avatar for Sansan, Inc. sansan33
PRO
1
3.1k
MCP Clientを活用するための設計と実装上の工夫
Avatar for Yudai Hayashi yudai00
1
800
AIとSREの未来 / AI and SRE
Avatar for ymotongpoo ymotongpoo
2
1.2k
MCP で繋ぐ Figma とデザインシステム〜LLM を使った UI 実装のリアル〜
Avatar for きむそん kimuson
2
1.3k
コードの考古学 〜労務システムから発掘した成長の糧〜
Avatar for Kenta SEKINE kenta_smarthr
1
1.2k
AIオンボーディングとAIプロセスマイニング
Avatar for Ryuya Nakamura nrryuya
5
1.3k
Eight Engineering Unit 紹介資料
Avatar for Sansan, Inc. sansan33
PRO
0
3.2k
ソフトウェアは捨てやすく作ろう/Let's make software easy to discard
Avatar for Genki Sano sanogemaru
10
5.8k

Featured

See All Featured
Code Review Best Practice
Avatar for Trisha Gee trishagee
68
18k
The Straight Up "How To Draw Better" Workshop
Avatar for Dennis Kardys denniskardys
233
140k
Embracing the Ebb and Flow
Avatar for Simon Collison colly
85
4.7k
Faster Mobile Websites
Avatar for Dean Hume deanohume
307
31k
Distributed Sagas: A Protocol for Coordinating Microservices
Avatar for Caitie McCaffrey caitiem20
331
21k
Save Time (by Creating Custom Rails Generators)
Avatar for Garrett Dimon garrettdimon
PRO
31
1.2k
A Tale of Four Properties
Avatar for Chris Coyier chriscoyier
159
23k
Art, The Web, and Tiny UX
Avatar for Lynn Fisher lynnandtonic
298
21k
Code Reviewing Like a Champion
Avatar for maltzj maltzj
523
40k
Refactoring Trust on Your Teams (GOTO; Chicago 2020)
Avatar for Rebecca Miller-Webster rmw
34
3k
Fontdeck: Realign not Redesign
Avatar for Paul Robert Lloyd paulrobertlloyd
84
5.5k
The Illustrated Children's Guide to Kubernetes
Avatar for Chris Short chrisshort
48
50k

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]