lthms.xyz/freespec.exec.org -rw-r--r-- 6.9 KiB View raw
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
---
title: Introduction to FreeSpec.Exec
abstract: "Gallina has long and infamously been known as “the language with no
           hello world.” FreeSpec.Exec is an attempt to improve this situation
           by making it way easier to execute Gallina specifications with
           side effects compared to prior approaches."

bg_color: "#f9f8f4"
font_color: "#0a0a0a"
primary_color: "#437087;"
code_bg_color: "#deeaef"
feature_img: "/img/freespec_feature.jpg"
credit: "A blueprint from <a
href=\"https://www.flickr.com/photos/internetarchivebookimages/14780705985/in/photolist-ou6hS9-ou6E73-oxTmga-ovR82t-oeCyCt-ovVgb9-ou5R5Y-oeC1zR-ow65cU-ovV4fA-ovV7ZQ-oeCh8d-oeCFuq-oeCkUG-ovUKEq-oeDeb9-oeCr2s-ow8H8M-ou6ShW-oeCHkZ-ovQS4H-oeD2TF-ow7YWn-ou6nnG-oxTGdV\">a
book from 1910</a>, Public Domain"

category: research
---

*The present document remains a draft and must be considered as such.*

Coq notably provides a nice purely functional language with dependent type
called Gallina to write specifications, and facilities (including a tactic
language called Ltac) to reason about their correctness.  Unfortunately, Gallina
has long and infamously been known as “the language with no hello world.”
Although Coq has a nice feature called /program extraction/ to turn Gallina
specifications into executable Ocaml programs, it has remained cumbersome to
use. The result of this situation is the small amount of “Coq flagship
projects” (/eg./ [[https://compcert.inria.fr][CompCert]]).

FreeSpec.Exec, an extensible plugin provided by the [[https://github.com/anssi-fr/freespec][FreeSpec framework]], is an
attempt to improve this situation by making it easy to execute Gallina
specifications with side effects with ~coqc~ only. There is no need to deal with
extraction-related burden anymore.

For instance, here is how you write a hello world program in Coq using
FreeSpec.Exec.

#+BEGIN_SRC coq
Require Import FreeSpec.Program.
Require Import FreeSpec.Stdlib.Console.

Definition hello {ix} `{Use Console.i ix}
  : Program ix unit :=
  Console.echo "Hello, world!".

Exec hello.
#+END_SRC

And executing this program is simply a matter of calling ~coqc~.

#+BEGIN_SRC bash
$ coqc hello.v
Hello, world!
#+END_SRC

* Getting Started

FreeSpec.Exec remains in an early stage of development. While the core of the
plugin already works as intended, too few useful interfaces are supported at the
moment.

Fortunately, because FreeSpec.Exec is /extensible/, you can already start
experimenting with it by defining your own interfaces.

* Extending FreeSpec.Exec

FreeSpec.Exec is /extensible/, meaning it is easy for Coq developers to define
their interfaces, implement primitive semantics in dedicated OCaml plugins, and
enjoy ~coqc~ being able to execute programs written thanks to these primitives.

** Defining Effectful Semantics

In FreeSpec, primitives are modeled with Coq terms, and in FreeSpec.Exec, an
~effectful_semantic~ of a given primitive is an OCaml function which computes a
result given the list of arguments of a particular primitive.

In FreeSpec.Exec, ~effectful_semantic~ is defined in OCaml as follows:

#+BEGIN_SRC ocaml
type effectful_semantic =
  Constr.constr list -> Constr.constr
#+END_SRC

… where the ~Constr.constr~ type (as defined in the Coq source in the
[[https://github.com/coq/coq/blob/master/kernel/constr.ml][kernel/constr.ml]] file) allows for describing (and manipulating) Coq
terms. Hopefully, you should not have to learn how Coq works under the hood and
~Constr.constr~ in particular, as FreeSpec.Exec intends to provide facilities to
fill the gap between Coq and OCaml world.

#+CAPTION: From Coq to OCaml and back
#+NAME: tbl:ocaml-coq-conv
  | Coq      | OCaml    | to OCaml            | from OCaml         |
  |----------+----------+---------------------+--------------------|
  | ~Z~      | ~int~    | ~int_of_coqz~       | ~int_to_coqz~      |
  | ~bool~   | ~bool~   | ~bool_of_coqbool~   | ~bool_to_coqbool~  |
  | ~ascii~  | ~char~   | ~char_of_coqascii~  | ~char_to_coqascii~ |
  | ~string~ | ~bytes~  | ~bytes_of_coqascii~ | ~bytes_to_coqstr~  |
  | ~string~ | ~string~ |                     | ~string_to_coqstr~ |
  | ~unit~   |          |                     | ~coqtt~            |

Let’s have a look with a concrete example. FreeSpec comes with a simple package
called FreeSpec.Stdlib.Console whose purpose is to provide simple primitives to
read from the standard input and write to the standard output.

The interface in ~FreeSpec.Stdlib.Console~ is defined as follows:

#+BEGIN_SRC coq
Module Console.
  Inductive i: Type -> Type :=
  | Scan: i string
  | Echo: string -> i unit.
End Console.
#+END_SRC

~Scan~ of type ~Console.i unit~ is intended to be a primitive to read one line
from the standard input, while ~Echo s~ of type ~Echo unit~ is inteded to be the
primitive to write the string ~s~ into the standard output.

In FreeSpec.Stdlib.Console, the effectful semantic of scan is implemented as
follows:

#+BEGIN_SRC ocaml
let scan = function
  | [] -> string_to_coqstr (read_line ())
  | _ -> assert false
#+END_SRC

We convert the result of ~read_line ()~ (of OCaml type ~string~) into a
~Constr.constr~ value using ~string_to_coqstr~. Because ~scan~ does not have any
parameter, we raise an error if a non-empty list is passed to us as input. In
such a case, this means there is a bug in FreeSpec.Exec, or that the Coq
definition of ~Scan~ as been changed.

The ~effectful_semantic~ of ~Echo~ is not harder to write:

#+BEGIN_SRC ocaml
let echo = function
  | [str] -> print_bytes (bytes_of_coqstr str);
             coqtt
  | _ -> assert false
#+END_SRC

We convert the Coq term passed as an argument of ~Echo~ using ~bytes_of_coqstr~,
then we send it to the standard output using ~print_bytes~. We then return a Coq
term (~tt~) whose ~Constr.constr~ representation in OCaml is ~coqtt~.

** Registering with FreeSpec.Exec

Now that we have defined effectful semantics for the primitives of ~Console.i~,
we have everything we need to emulate in OCaml the missing piece of ~Program~
evaluation, that is a function of type:

#+BEGIN_SRC coq
forall {A: Type}, Console.i A -> A
#+END_SRC

The next and last step is to let FreeSpec.Exec know about these semantics (“to
register our ~effectful_semantics~ to FreeSpec.Exec”).

The ~Extends~ module provides a function to that end:

#+BEGIN_SRC ocaml
val register_interface :
 (* The path of the module within the interface type
    lives. *)
    string list
 (* A list to map each constructor of this interface
    to an effectfull semantic. *)
 -> (string * effectful_semantic) list
 -> unit
#+END_SRC

The type signature of ~register_interface~ is pretty self-explanatory.

#+BEGIN_SRC ocaml
let _ =
  register_interface
    ["FreeSpec"; "Stdlib"; "Console"; "Console"]
    [("Scan", scan); ("Echo", echo)]
#+END_SRC

* Conclusion

FreeSpec.Exec provides a novel approach to turn Gallina into a real programming
language. It currently lacks a comprehensive library of primitives, but it is
/extensible/ so that you do not have to wait for us to start testing it.