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

Programming Languages x Blockchains

Sponsored · Ship Features Fearlessly Turn features on and off without deploys. Used by thousands of Ruby developers. →
Avatar for Volodymyr Kyrylov Volodymyr Kyrylov
April 25, 2018
Technology
280
1

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

More Decks by Volodymyr Kyrylov

See All by Volodymyr Kyrylov
Ur/Web: lightning fast prototyping for the web
Avatar for Volodymyr Kyrylov proger
0
280
Swift to Haskell: Overloading Semicolons
Avatar for Volodymyr Kyrylov proger
2
280
The Programming Language of Mathematics
Avatar for Volodymyr Kyrylov proger
3
710
Stochastic Relaxation, Gibbs Distributions, and the Bayesian Restoration of Images
Avatar for Volodymyr Kyrylov proger
0
1.2k
Monosyn - monocular navigation for robots
Avatar for Volodymyr Kyrylov proger
0
180
Lambda the Ultimate Devops v2
Avatar for Volodymyr Kyrylov proger
1
530
Lambda the Ultimate Devops
Avatar for Volodymyr Kyrylov proger
0
310
Haskell >>= DevOps
Avatar for Volodymyr Kyrylov proger
0
990
The Zalora Platform
Avatar for Volodymyr Kyrylov proger
2
930

Other Decks in Technology

See All in Technology
FPGAの開発コンペでZephyrを使ってみた
Avatar for misoji engineer iotengineer22
0
200
AIAU_UMEMOGU_ninomiya_slide
Avatar for ninomiya ninomiya_ii
0
260
From Prompt Engineering to Loop Engineering
Avatar for shibuiwilliam shibuiwilliam
1
220
サイバーエージェントにおけるAI推進戦略と変革への取り組み
Avatar for shotaTsuge shotatsuge
0
560
AIが自律的に回る開発ループを設計してチーム開発に組み込む
Avatar for Mitsuhiro Komuro (nekorush14) nekorush14
0
130
AIをフル活用してオンコール機能のプロトタイプを2日で作った話 / Building an AI-Powered On-Call Prototype in Just Two Days
Avatar for Narimichi Takamura nari_ex
0
130
2026年6月23日 Syncable Tech + Start Python Club にて
Avatar for Kimikazu Kato hamukazu
0
150
Agile and AI Redmine Japan 2026
Avatar for Kenji Hiranabe hiranabe
4
480
Zenoh on Zephyr on LiteX
Avatar for takasehideki takasehideki
2
110
AIチャットの改善から見えた、良いAI体験とは / What Constitutes a Good AI Experience: Insights from Improving AI Chat
Avatar for Masatoshi Kubode kubode
0
120
AIネイティブな開発のサプライチェーンリスク対策 〜激動の開発現場でリスクに立ち向かう〜【ZennFes】
Avatar for サイバーセキュリティクラウド cscengineer
PRO
2
160
GitHub Copilot app最速の発信の裏側
Avatar for tomokusaba tomokusaba
1
260

Featured

See All Featured
16th Malabo Montpellier Forum Presentation
Avatar for AKADEMIYA2063 akademiya2063
PRO
0
150
Context Engineering - Making Every Token Count
Avatar for Addy Osmani addyosmani
9
980
Are puppies a ranking factor?
Avatar for Jono Alderson jonoalderson
1
3.6k
Code Reviewing Like a Champion
Avatar for maltzj maltzj
528
40k
Stewardship and Sustainability of Urban and Community Forests
Avatar for Eric Wiseman pwiseman
0
230
The agentic SEO stack - context over prompts
Avatar for schlessera schlessera
0
820
No one is an island. Learnings from fostering a developers community.
Avatar for Antonio thoeni
21
3.8k
Navigating the Design Leadership Dip - Product Design Week Design Leaders+ Conference 2024
Avatar for Andy Polaine apolaine
1
360
brightonSEO & MeasureFest 2025 - Christian Goodrich - Winning strategies for Black Friday CRO & PPC
Avatar for Christian Goodrich cargoodrich
3
740
Building Better People: How to give real-time feedback that sticks.
Avatar for Will Jessup wjessup
370
20k
Practical Tips for Bootstrapping Information Extraction Pipelines
Avatar for Matthew Honnibal honnibal
25
2k
Paper Plane
Avatar for Katie Cordina Lindsey katiecoart
PRO
1
52k

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]