February 20, 2015
The Hello World program exists in almost every languages, including in White Space. In Coq this is more complicated because the language is purely functional. This means that no effects can be done, in particular no inputs-outputs. This constraint is there to preserve the logical consistency of the system. However, we can still encode inputs-outputs by defining a monad. This technique was popularized by the Haskell programming language.
opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-io-system
You can now write the Hello World:
Require Import Coq.Lists.List. Require Import Io.All. Require Import Io.System.All. Require Import ListString.All. Import ListNotations. Import C.Notations. (** The classic Hello World program. *) Definition hello_world (argv : list LString.t) : C.t System.effect unit := System.log (LString.s "Hello world!").
We load some libraries and write the
hello_world program by calling the
System.log function. The return type is
C.t System.effect unit, which means this is a impure computation with System effects and returning a value of type
unit. The command line arguments are given in the list of strings
argv, but not used here.
To compile the
hello_world program we add:
Definition main := Extraction.launch hello_world. Extraction "extraction/main" main.
to generate an OCaml file
main.ml. We compile and run this file:
ocamlbuild main.native -use-ocamlfind -package io-system ./main.native
This should display
Hello world! on the terminal.
The specification of this program is very straightforward: the program only prints “Hello world!” and quits (here the specification is as long as the program itself, but this is not always the case). A simple way to write this specification is to describe an environment of the program which reacts to a single event: the printing of the message “Hello world!” on the terminal. You can express this environment as a program:
(** The Hello World program only says hello. *) Definition hello_world_ok (argv : list LString.t) : Run.t (hello_world argv) tt. apply (Run.log_ok (LString.s "Hello world!")). Defined.
hello_world_ok is of type
Run.t (hello_world argv) tt: this runs the program
hello_world on an argument
argv and returns the result
tt. We just apply the function
Run.log_ok of the coq-io-system library which exactly describes an environment reacting to a single printing event.
This specification needs no proofs because it is valid by construction. We do not need any SMT solver, model checker or manual proof. The specification is valid because it is well-typed. Of course this example is very simple, so we will see a slightly more complex one.
This program asks for your name and replies with your name:
(** Ask for the user name and answer hello. *) Definition your_name (argv : list LString.t) : C.t System.effect unit := do! System.log (LString.s "What is your name?") in let! name := System.read_line in (* Ask the name. *) match name with | None => ret tt (* In case of error do nothing. *) | Some name => System.log (LString.s "Hello " ++ name ++ LString.s "!") end.
We see here how to compose impure computations in sequence with the
let! keywords. The construct:
let! x := e1 in e2
e1, assigns the result to
x and then executes
do! is a syntactic sugar for a
let! with an empty variable name. We use the
System.read_line function which gets a new line on the standard input. If the
read_line operation fails we returns the pure value
tt using the
ret operator, else we print the user name on the terminal.
You can run this program as before by compilation to OCaml.
We have two use cases for the
For the first use case:
(** The `your_name` program answers something when you give your name. *) Definition your_name_ok (argv : list LString.t) (name : LString.t) : Run.t (your_name argv) tt. apply (Run.Let (Run.log_ok _)). apply (Run.Let (Run.read_line_ok name)). apply (Run.log_ok _). Defined.
The specification is parametrized by a
name which could be any string. The environment does exactly three steps:
_means any value)
nameto the event
Run.Let command composes two steps. For a failing standard input:
(** The `your_name` program does nothing more in case of error on stdin. *) Definition your_name_error (argv : list LString.t) : Run.t (your_name argv) tt. apply (Run.Let (Run.log_ok _)). apply (Run.Let Run.read_line_error). apply Run.Ret. Defined.
we also give three steps:
Again, we do not need to prove anything because the specifications are correct by construction.
Next time we will continue with more tutorials, to help you build and certify realistic interactive applications in Coq.blog comments powered by Disqus