---
# System prepended metadata

title: Smart Contracts

---

<div style="display: flex; align-items:center;flex-direction: column;">
<img src="https://hackmd.io/_uploads/HyyVnQv3T.png"/>
<h1>Interoperability </h1>
</div>

<hr style="page-break-after: always;"/>

<img src="https://hackmd.io/_uploads/By3udS3A6.png"/>

# Smart Contracts


## Cardano

The original language/technology is called Plutus (named after the Greek god of wealth).
Plutus compiles to UPLC (untyped plutus core) bytecode.
Languages that compile to UPLC:
- Haskell (specific subset)
- Plutarch (Haskell library)
- Aiken (https://aiken-lang.org/) (getting more and more "exposure")
- Pluto (not widely used)
- Plu-ts (typescript library)
- Helios

Plutus Pioneer program: IOG organized learning course.

### Sidenote: FFP vs OOP 
- Easy to rationalize, easier to proof, easier to scale more bugfree
- Speaking to a mathematician, specific, runs what i say it runs
- OOP game thingy thinking fits well
- OOP comes from UI (smalltalk invited that)
- OOP went nuts 199X and it was thee thiiing, then everyone realized doesnt not fit all problems, DesignPatterns invention time, .. 

### Sidenote: Education

- [Plutus Pioneer Program](https://docs.cardano.org/pioneer-programs/plutus-pioneers/)
- [Giovanni videos](https://www.youtube.com/watch?v=z5_1WiVc3aA)
- [Plutonomicon](https://github.com/Plutonomicon)
- [Plutus repo](https://github.com/input-output-hk/plutus)
- [Cardano Ledger repo](https://github.com/input-output-hk/cardano-ledger)
- [Plutus Apps](https://github.com/input-output-hk/plutus-apps)

### Sidenote: Formal verification
- Coq
- Languages used in Coq source files: Vernacular, Gallina, Ltac.
- Use cases of formal verification/formal methods.
- Formal verification is the process of prooving properties of an already existing program.
- Formal methods is a way to create programs that are formally verified.
- Strong use cases for formal methods/verifications:
    - Healthcare
    - Automotive
    - Finances (blockhain!)

### Sidenote: stack vms vs lambda calculus based vms
- Stack based vms mainly operate on values stored in a stack. [https://www.evm.codes/playground]
- Currently only one blockchain uses a lambda calculus based vm: Cardano.
- Lambda calculus based vm is easier to reason about => formal verification

### Sidenote: dependent types
- Types that can depend on values are called dependent types.
- Haskell does not have dependent types, Coq has, so value and types live in the same "universe".

### Sidenote: setting up nix and nix flakes
- (nix)[https://nixos.org/download/]
- (nix flakes)[https://nixos.wiki/wiki/Flakes]

### Sidenote: Cabal, Haskell, GHC, Stack
- Cabal is the canonical package manager and build system for Haskell.
- Stack is a newer build system, it uses cabal under the hoods.

### Sidenote: example of datum
- https://cardanoscan.io/transaction/352037be78ea223514d3982f1a06186b1d4036046c14245d4be8e0aa62f698a2?tab=utxo

### Sidenote: deterministic transactions

### Sidenote: blockchain state in Cardano

### Sidenote: Validation if transactions

### Sidenote: Plutus versions

### Sidenote: Data types

### Aiken
- (Aiken language)[https://aiken-lang.org]

### Sidenote: Validation script are passive in Cardano

### Sidenote: Stacks - smart contracts for Bitcoin
