Tutorials

• 1: Writing Proof with Witch
• 2: Multi-Bear Domicile Setup
• 3: Another Tutorial
• 4: Syntax-Guide

1 - Writing Proof with Witch

Writing proofs in Juvix

To popularise software verification, we must make proof writing less of a burden on you, the user. Currently, only specialists and a few others can write proofs for their programs, even though you surely understand the domain and invariants of your projects – otherwise you wouldn’t be able to write any software at all.

Our hypothesis is that programmers are well-equipped to derive and prove properties of the software they write, but they lack the mathematical maturity and vocabulary to carry out a formal proof. We have evidence that students fail to produce well-made proofs due to the lack of mathematical maturity, even though they do understand the subject matter at hand.

We believe that program verification doesn’t have to be like this, and we did something about it. We created an assistant tool for theorem provers that puts together many different strategies for proof automation. Our specification for such an assistant for Juvix uses algebraic effects and handlers as the means of congregation.

The approach to facilitate program verification in Juvix is named Witch, a play on the name of assistant tools colloquially called “wizards”. There is no consensus of what a wizard is or what the exact tasks it is supposed to assist with. Wizards seem to be used mostly for multiple-step and/or configuration features, however. We went for the name “witch” to align it to the idea of assistant tools, while dodging the overloaded and confusing terminology.

We propose an effects and handlers view of such proofs, based on prior work developed on the Andromeda prover.
In Juvix, you program as you would normally and invoke the proof environment as an effect to prove certain properties as you go. Given that the proof environment is just an effect, different proof styles (e.g., Agda-style dependent types, SMT solver, proof search) can be composed under a shared interface, a proof object that can manipulate itself while querying different automated provers.

The reasons we employ algebraic effects and handlers are numerous:

1. as proofs cannot be fully automated, all approaches that try to automate the process (e.g, proof search, SMT solver) may be non-deterministic or never find a solution. Therefore, the system should be able to handle “impure” computations and errors. Algebraic effects and handlers have well-defined semantics and provide a simple interface for performing effects. With them, we avoid indiscriminate effects that are often error-prone and intricate effects machinery such as monad transformers;

2. the semantics of effects and handlers accommodate composition of arbitrary effects and the composition of multiple handlers, which means users have the ability to weaken more general strategies into specific ones while maintaining top-level handlers unmodified;

3. effects and handlers have well-defined semantics, and it is the main feature of many new languages, such as Koka, Eff, Frank and Effekt, and have implementation in all major functional programming languages. This guarantees that our approach is based in research and real-world experiences, and not something we hacked together over the weekend.

The Essence of Witch

As for the syntax, we use operation { params } via handler, which is semantically equivalent to but a syntactic improvement over handler(operation, params), since effect handling is similar to function application, but also carries effect information. The user defines data types and functions as usual, and then uses Witch to prove properties about said definitions. The examples below show it in action:

data ℕ : Type where
  0 : ℕ 
  s : ℕ → ℕ
  
  _+_       : ℕ → ℕ → ℕ
  0 + n     = n
  (s m) + n = suc (m + n)

+comm          : ∀ (x y : ℕ) → Witch x + y ≡ y + x
+comm 0 y     = tactic { 0 + y ≡ y + 0 } via Ring
+comm (s x) y = search { x + (s y) ≡ suc (x + y) } via Backtracking


++assoc         : ∀ {A : Set} (x y z: [A]) → Witch (x ++ y) ++ z ≡ x ++ (ys ++ zs)
++assoc ∅ y z   = solve { (∅ ++ y) ++ z ≡ ∅ ++ (ys ++ zs) } via SMT 
++assoc (x ∷ xs) y z rewrite ++assoc xs y z 
                = pure ref

The proof of commutativity of addition under natural numbers and of associativity of list concatenation are shown, and use the three main effects: Solver, Proof Search and Tactics. In the proof assistant literature, there exists no precise definition of commonly used terms “solver”, “proof search” and “tactics”. All these terms are used in different communities, and mean some variation of “automatic strategy to construct a term under certain constraints”.

In Witch, however, we use the following definitions of previously known terms:

• The Solver effect is used for integration with external solvers via IO; we believe it should suffice for the user to write, e.g. SMT, and handlers should implement internal strategies to choose between the different theories supported by solvers. If the black-box approach to solvers presents itself a challenge, a specialisation of the handler is possible, e.g. operation { params } via Z3.QF-UFLIA .

• The Proof Search effect is used for library-level algorithms; users may choose to implement their own algorithms using a limited set of meta-programming¹ constructs that are handled at top-level².

• The Tactics effect is used for strategies that simplify the goal at least one step, and may not complete all proof goals. This style is mainly used in the proof assistant Coq. While we do not foresee using as many as many tactics implemented as in Coq, we believe tactics such as eauto, rewrite, unfold are useful to users of all levels of expertise.

• Lastly, the Error effect is used for feedback to the user, since any of the strategies may fail. Error has two operations, throw and trace: the former notifies the user that a strategy has failed, while the latter registers³ completed sub-goals during the strategy’s attempt to complete the proof.

Witch for Juvix is currently under development, and we hope to release its first version soon. :)

¹ By meta-programming, we mean “code that manipulates itself”, and not “programming that happens in a higher level of abstraction”. For dependently typed programming languages, the usual term is reflection. However, we prefer not use reflection since it has a different meaning in terms of effectful computations.

² The meta-programming constructs are operations of the Typechecker effect whose handlers are not available for the user.

³ Internally, the Typechecker effect should have a tree that stores all currently saved traces.

2 - Multi-Bear Domicile Setup

Text can be bold, italic, or strikethrough. Links should be blue with no underlines (unless hovered over).

There should be whitespace between paragraphs. Vape migas chillwave sriracha poutine try-hard distillery. Tattooed shabby chic small batch, pabst art party heirloom letterpress air plant pop-up. Sustainable chia skateboard art party banjo cardigan normcore affogato vexillologist quinoa meggings man bun master cleanse shoreditch readymade. Yuccie prism four dollar toast tbh cardigan iPhone, tumblr listicle live-edge VHS. Pug lyft normcore hot chicken biodiesel, actually keffiyeh thundercats photo booth pour-over twee fam food truck microdosing banh mi. Vice activated charcoal raclette unicorn live-edge post-ironic. Heirloom vexillologist coloring book, beard deep v letterpress echo park humblebrag tilde.

90’s four loko seitan photo booth gochujang freegan tumeric listicle fam ugh humblebrag. Bespoke leggings gastropub, biodiesel brunch pug fashion axe meh swag art party neutra deep v chia. Enamel pin fanny pack knausgaard tofu, artisan cronut hammock meditation occupy master cleanse chartreuse lumbersexual. Kombucha kogi viral truffaut synth distillery single-origin coffee ugh slow-carb marfa selfies. Pitchfork schlitz semiotics fanny pack, ugh artisan vegan vaporware hexagon. Polaroid fixie post-ironic venmo wolf ramps kale chips.

There should be no margin above this first sentence.

Blockquotes should be a lighter gray with a border along the left side in the secondary color.

There should be no margin below this final sentence.

First Header 2

This is a normal paragraph following a header. Knausgaard kale chips snackwave microdosing cronut copper mug swag synth bitters letterpress glossier craft beer. Mumblecore bushwick authentic gochujang vegan chambray meditation jean shorts irony. Viral farm-to-table kale chips, pork belly palo santo distillery activated charcoal aesthetic jianbing air plant woke lomo VHS organic. Tattooed locavore succulents heirloom, small batch sriracha echo park DIY af. Shaman you probably haven’t heard of them copper mug, crucifix green juice vape single-origin coffee brunch actually. Mustache etsy vexillologist raclette authentic fam. Tousled beard humblebrag asymmetrical. I love turkey, I love my job, I love my friends, I love Chardonnay!

Deae legum paulatimque terra, non vos mutata tacet: dic. Vocant docuique me plumas fila quin afuerunt copia haec o neque.

On big screens, paragraphs and headings should not take up the full container width, but we want tables, code blocks and similar to take the full width.

Scenester tumeric pickled, authentic crucifix post-ironic fam freegan VHS pork belly 8-bit yuccie PBR&B. I love this life we live in.

Second Header 2

This is a blockquote following a header. Bacon ipsum dolor sit amet t-bone doner shank drumstick, pork belly porchetta chuck sausage brisket ham hock rump pig. Chuck kielbasa leberkas, pork bresaola ham hock filet mignon cow shoulder short ribs biltong.

Header 3

This is a code block following a header.

Next level leggings before they sold out, PBR&B church-key shaman echo park. Kale chips occupy godard whatever pop-up freegan pork belly selfies. Gastropub Belinda subway tile woke post-ironic seitan. Shabby chic man bun semiotics vape, chia messenger bag plaid cardigan.

Header 4

• This is an unordered list following a header.
• This is an unordered list following a header.
• This is an unordered list following a header.

Header 5

1. This is an ordered list following a header.
2. This is an ordered list following a header.
3. This is an ordered list following a header.

Header 6

There’s a horizontal rule above and below this.

Here is an unordered list:

• Liverpool F.C.
• Chelsea F.C.
• Manchester United F.C.

And an ordered list:

1. Michael Brecker
2. Seamus Blake
3. Branford Marsalis

And an unordered task list:

• Create a Hugo theme
• Add task lists to it
• Take a vacation

And a “mixed” task list:

• Pack bags
• ?
• Travel!

And a nested list:

• Jackson 5
  • Michael
  • Tito
  • Jackie
  • Marlon
  • Jermaine
• TMNT
  • Leonardo
  • Michelangelo
  • Donatello
  • Raphael

Definition lists can be used with Markdown syntax. Definition headers are bold.

Name

Godzilla

Born

1952

Birthplace

Japan

Color

Green

Tables should have bold headings and alternating shaded rows.

If a table is too wide, it should scroll horizontally.

Code snippets like var foo = "bar"; can be shown inline.

Also, this should vertically align with this and this.

Code can also be shown in a block element.

foo := "bar";
bar := "foo";

Code can also use syntax highlighting.

func main() {
  input := `var foo = "bar";`

  lexer := lexers.Get("javascript")
  iterator, _ := lexer.Tokenise(nil, input)
  style := styles.Get("github")
  formatter := html.New(html.WithLineNumbers())

  var buff bytes.Buffer
  formatter.Format(&buff, style, iterator)

  fmt.Println(buff.String())
}

Long, single-line code blocks should not wrap. They should horizontally scroll if they are too long. This line should be long enough to demonstrate this.

Inline code inside table cells should still be distinguishable.

Small images should be shown at their actual size.

Large images should always scale down and fit in the content container.

The photo above of the Spruce Picea abies shoot with foliage buds: Bjørn Erik Pedersen, CC-BY-SA.

Components

Alerts

Another Heading

Add some sections here to see how the ToC looks like. Bacon ipsum dolor sit amet t-bone doner shank drumstick, pork belly porchetta chuck sausage brisket ham hock rump pig. Chuck kielbasa leberkas, pork bresaola ham hock filet mignon cow shoulder short ribs biltong.

This Document

Inguina genus: Anaphen post: lingua violente voce suae meus aetate diversi. Orbis unam nec flammaeque status deam Silenum erat et a ferrea. Excitus rigidum ait: vestro et Herculis convicia: nitidae deseruit coniuge Proteaque adiciam eripitur? Sitim noceat signa probat quidem. Sua longis fugatis quidem genae.

Pixel Count

Tilde photo booth wayfarers cliche lomo intelligentsia man braid kombucha vaporware farm-to-table mixtape portland. PBR&B pickled cornhole ugh try-hard ethical subway tile. Fixie paleo intelligentsia pabst. Ennui waistcoat vinyl gochujang. Poutine salvia authentic affogato, chambray lumbersexual shabby chic.

Contact Info

Plaid hell of cred microdosing, succulents tilde pour-over. Offal shabby chic 3 wolf moon blue bottle raw denim normcore poutine pork belly.

External Links

Stumptown PBR&B keytar plaid street art, forage XOXO pitchfork selvage affogato green juice listicle pickled everyday carry hashtag. Organic sustainable letterpress sartorial scenester intelligentsia swag bushwick. Put a bird on it stumptown neutra locavore. IPhone typewriter messenger bag narwhal. Ennui cold-pressed seitan flannel keytar, single-origin coffee adaptogen occupy yuccie williamsburg chillwave shoreditch forage waistcoat.

This is the final element on the page and there should be no margin below this.

3 - Another Tutorial

4 - Syntax-Guide

  -- this is a function with a signature!
  sig foo : Natural
  let foo = 3

  -- this is a data type declaration
  type list a = Cons a (List a)
              | Nil

  -- this is a module declaration!
  mod Boo =
    let fi = 10
  end

  -- This is a comment!

  -- a valid symbol
  hello-there

  -- another valid symbol
  _unused-symbol

  -- another valid symbol. Typically '?' denotes that the symbol is a predicate
  even?

  -- An important action
  foo!

  -- not a valid prefix symbol
  -foo

  -- This is a valid infix symbol

  !!

  -- this is also another valid infix symbol

  -<++

  -- this is not a valid infix symbol, but instead a comment of a -

  ---

  -- here is an arrow infix symbol

  ->

  -- this is a valid function
  let f x = x + 3

  -- this is another valid variable/function
  let y = 5

  -- this is a valid infix symbol
  let (+) = plus


  -- a function with an implicit argument
  let foo {prf} x = x

  -- a valid signature and function
  sig foo : int -> int
  let foo x = x + 3


  -- an example of a dependent signature
  sig add-nat-int
      :  x : nat
      -> y : int
      -> if | x > y -> nat
            | else  -> int
  let add-nat-int = (+)

  -- This is a valid type
  -- the a is a type argument
  type list a
    -- Cons is the constructor
    -- Cons takes an item of type a and a List of a
    = Cons a (list a)
    -- Nil is another constructor taking no arguments
    | Nil


  -- this is the same type, but GADT style arrow syntax
  -- is given to the constructor
  type list a : a -> list a
  -- Curly braces can be used here to name the arguments
    = Cons { car : a,
             cdr : list a }
    | Nil

  -- Same type again but using GADT syntax in the constructors
  -- The first product can have a pipe!
  type list a =
    | Cons : a -> list a -> list a
    | Nil  : list a

  -- an example of a base record!
  type coords a = {
    x : a,
    y : a
  }

  -- Same example but we have a trailing comma
  type cords a = {
    x : a,
    y : a,
  }

  -- An example of a dependent type
  type vect : (len : nat) -> (elem : set) -> set =
    | Nil  : vect 0 elem
    | Cons : elem -> vect len elem -> vect (succ len) elem

  -- example defining a module

  mod Foo =
    sig bar : nat
    let bar = 3

    -- The type is inferred here
    let baz = 5

  -- end ends the module definition
  end

  -- example using a module
  let test = Foo.bar + Foo.baz

  -- A valid open
  open Foo

  -- opening the module Baz in the moudle Bar in the moudle Bar
  open Foo.Bar.Baz

  -- This is the same statement as above.
  open Foo
  open Bar.Baz


  -- let us define a module
  mod IntMod =
    let t = int

    sig of-nat : int -> t
    let of-nat x = x

    sig add : t -> t -> t
    let add = (+)
  end

  -- now we shall open it into our scope
  open IntMod

  -- we can now use it unqualified
  sig use-int-mod : nat -> nat -> t
  let use-int-mod x y = add (of-nat x) (of-nat y)

  -- a valid module alias
  let F = Foo

  -- this is a valid if expression!
  if | x == 3 -> 5
     | else   -> 6
  -- ^ test      ^ consequence

  -- this is also a valid a valid if expression
  if | x == 10     -> 25
     | positive? x -> x
     | negative? x -> abs x
     | else        -> 0

  type tree a = Branch (tree a) a (tree a)
              | Leaf a
              | Empty


  -- an example with match!
  sig func : Tree nat -> nat
  let func foo =
    case foo of
    | Branch left ele right ->
      func left + ele + func right
    | Leaf ele ->
      ele
    | Empty ->
      0

  -- This is the same function!
  let func2 (Branch left ele right) =
    func2 left + ele + func2 right
  let func2 (Leaf ele) =
    ele
  let func2 Empty =
    0

  type coords = {
    x : int,
    y : int
  }

  -- match on record

  sig origin? : coords -> boolean
  let origin? {x, y}
    | x == y && x == 0 = True
    | else             = False

  -- same function as origin
  sig origin2? : coords -> boolean
  let origin2? {x = origX, y = origY}
    | origX == origY && origX == 0 =
      True
    | else = False

  let foo =
    let bar = 3 in
    bar + 10

  let foo =
    mod Bar =
      let foo = 3
      let bat = 10
    end in
    Bar.foo + Bar.bat

  let foo =
    type bar = Foo int
             | Bar nat
    in [Foo 3, Bar 10]

  -- this is a valid list
  [1]

  -- another valid list
  [1,2,3]

  -- the same list without sugar
  Cons 1 (Cons 2 (Cons 3 Nil))

  -- this is a tuple
  (1, 2)

  -- this is not a tuple
  (1)

  -- this is a 5 tuple!
  (1,2,3,4,5)

  type coords = {
    x : int,
    y : int
  }

  -- a new construct called foo for coords
  sig create-cords : int -> int -> coords
  let create-cords x-dir y-dir = {
    x = x-dir,
    y = y-dir
  }


  -- same function with punning
  sig create-cords : int -> int -> coords
  let create-cords x y = {x, y}

  let foo =
    "this is a string!"

  -- a valid number literal
  let foo = 123


  -- another valid number
  let number-one = 1

  let foo my =
    x <- Just 5;
    y <- my;
    pure (x + y)


  let bar =
    Out.print "hello";
    name <- In.prompt "What is your name";
    Out.print ("hello" <> name)

  let foo xs ys zs =
    open List in
    append xs (append ys zs)

  let foo xs ys zs =
    List.(append xs (append ys zs))