diff options
| author | Thomas Letan <lthms@soap.coffee> | 2023-05-13 16:12:57 +0200 |
|---|---|---|
| committer | Thomas Letan <lthms@soap.coffee> | 2023-05-13 16:12:57 +0200 |
| commit | 3dd38b1d3f4fe3fafa180f6fcb0d4fb9c39e1706 (patch) | |
| tree | 8d510bd97021bbbdbe4b171d62e77eceb2863d90 | |
| parent | A favicon finally! (diff) | |
Antidote to the rescue
24 files changed, 215 insertions, 214 deletions
diff --git a/site/posts/AlgebraicDatatypes.md b/site/posts/AlgebraicDatatypes.md index e52306d..baeec43 100644 --- a/site/posts/AlgebraicDatatypes.md +++ b/site/posts/AlgebraicDatatypes.md @@ -65,9 +65,9 @@ types. b$ is made of one term of $a$ and one term of $b$ (think tuples). For an algebraic datatype, one constructor allows for defining “named -tuples”, that is ad-hoc product types. Besides, constructors are mutually +tuples,” that is ad hoc product types. Besides, constructors are mutually exclusive: you cannot define the same term using two different constructors. -Therefore, a datatype with several constructors is reminescent of a disjoint +Therefore, a datatype with several constructors is reminiscent of a disjoint union. Coming back to the $\mathrm{list}$ type, under the syntactic sugar of algebraic datatypes, we can define it as @@ -120,7 +120,7 @@ we will have to prove they are “equivalent.” Since `=`{.coq} for `Type`{.coq} is not suitable for reasoning about algebraic datatypes, we introduce our own equivalence relation, denoted `==`{.coq}. We say two types $\alpha$ and $\beta$ are equivalent up to an isomorphism -when for any term of type $\alpha$, there exists a counter-part term of type +when for any term of type $\alpha$, there exists a counterpart term of type $\beta$ and vice versa. In other words, $\alpha$ and $\beta$ are equivalent if we can exhibit two functions $f$ and $g$ such that: @@ -294,7 +294,7 @@ the form `α == β`{.coq} with the `rewrite` tactic. I personally consider providing instances of `Proper`{.coq} whenever it is possible to be a good practice, and would encourage any Coq programmers to do so. -#### `nat`{.coq} is a special-purpose `list` +#### `nat`{.coq} is a special purpose `list` Did you notice? Now, using `type_equiv`{.coq}, we can prove it! @@ -387,7 +387,7 @@ Qed. ## The `sum`{.coq} Operator -### `sum`{.coq} Is A Morphism +### `sum`{.coq} Is a Morphism To prove this, we compose together the functions whose existence is implied by $\alpha = \alpha'$ and $\beta = \beta'$. To that end, we introduce the @@ -442,9 +442,9 @@ Qed. ### `sum`{.coq} Is Associative The associativity of `sum`{.coq} is straightforward to prove, and should not -pose a particular challenge to perspective readers[^joke]. +pose a particular challenge to prospective readers[^joke]. -[^joke]: If we assume that this article is well-written, that is. +[^joke]: If we assume that this article is well written, that is. ```coq Lemma sum_assoc {α β γ} : α + β + γ == α + (β + γ). @@ -482,7 +482,7 @@ Inductive empty := . [^empty]: Note that `Inductive empty.`{.coq} is erroneous. When the `:=`{.coq} is omitted, Coq defines an inductive type with one - constructor, making such a type a type equivalent to `unit`{.coq}, not + constructor, making such a type equivalent to `unit`{.coq}, not `False`{.coq}. From a high-level perspective, `empty`{.coq} being the neutral element of @@ -494,10 +494,10 @@ correct? Just like before, by providing two functions of types: - `α -> α + empty`{.coq} - `α + empty -> α`{.coq} -The first function is `inl`{.coq}, that is one of the constructor of +The first function is `inl`{.coq}, that is one of the constructors of `sum`{.coq}. -The second function is more tricky to write in Coq, because it comes down to +The second function is trickier to write in Coq, because it comes down to writing a function of type is `empty -> α`{.coq}. ```coq @@ -611,7 +611,7 @@ Qed. ### `prod`{.coq} Has An Absorbing Element *) And this absorbing element is `empty`{.coq}, just like the absorbing element of -the multiplication of natural number is $0$ (that is, the neutral element of +the multiplication of natural numbers is $0$ (that is, the neutral element of the addition). ```coq @@ -708,4 +708,5 @@ It is exactly what you could have expected (as match the type of Generating the body of the function is possible in theory, but probably not in `Ltac` without modifying a bit `type_equiv`{.coq}. This could be a nice -use-case for [MetaCoq](https://github.com/MetaCoq/metacoq) though. +use case for [MetaCoq](https://github.com/MetaCoq/metacoq) though. + diff --git a/site/posts/August2022.md b/site/posts/August2022.md index c0ff61b..c40a0c0 100644 --- a/site/posts/August2022.md +++ b/site/posts/August2022.md @@ -31,7 +31,7 @@ again[^minimalism]. The change I am the most excited about is that I have *finally* reduced the boilerplate in need to write to use a new theme. I am very indecisive when it comes to theming. I like to have my choices, and I get tired of any -colorscheme pretty quickly. As a consequence, I introduced a customizable +color scheme pretty quickly. As a consequence, I introduced a customizable variable to let me select a theme dynamically, and have this choice persist across Emacs session. @@ -71,7 +71,7 @@ things to me, instead of the echo area. The winning setup for now is the one that uses the [`quick-peek` package](https://github.com/cpitclaudel/quick-peek). That is, [`flycheck-inline`](https://github.com/flycheck/flycheck-inline) (customized to -use quick-peek, as suggested in their README), and +use `quick-peek`, as suggested in their README), and [`eldoc-overlay`](https://melpa.org/#/eldoc-overlay). This works well enough, so the pop-ups of eldoc are maybe a bit too distracting. @@ -79,7 +79,7 @@ so the pop-ups of eldoc are maybe a bit too distracting. In my quest for pop-ups, I ran into several issues with the packages I tried out. For instance, [`eldoc-box`](https://github.com/casouri/eldoc-box) was very -nice, but also very slow for some reason. It turns out there were an issue +nice, but also very slow for some reason. It turns out there was an issue about that slowness, wherein the culprit was identified. This allowed me to [submit a pull request that got merged rather quickly](https://github.com/casouri/eldoc-box/pull/48). @@ -112,7 +112,7 @@ the time to actually document them properly. ### Under the Hood Overall, the cost of using **`cleopatra`** was not worth the burden, and so I -got ride of it. Fortunately, it was not very difficult, since the job of +got rid of it. Fortunately, it was not very difficult, since the job of **`cleopatra`** was to extracting the generation processes from org files; I just add to implement a small `makefile` to make use of these files, without having to rely on **`cleopatra`** anymore. @@ -132,5 +132,5 @@ some point. Finally, I have created [a public mailing](https://lists.sr.ht/~lthms/public-inbox) list that is available if you -want to start a discussion on one of my article. Don’t hesitate to use it, or +want to start a discussion on one of my articles. Don’t hesitate to use it, or to register to it! diff --git a/site/posts/CFTSpatialShell.md b/site/posts/CFTSpatialShell.md index 14de1cd..602bd21 100644 --- a/site/posts/CFTSpatialShell.md +++ b/site/posts/CFTSpatialShell.md @@ -10,12 +10,12 @@ abstract: | # Spatial Shell: Call For Testers -In August, 2022, I have discovered [Material +In August 2022, I have discovered [Material Shell](https://material-shell.com). A few weeks later, I had pieced together a working prototype of a dynamic tiling management “a la Material Shell” for [sway](https://swaywm.org). By October, the project was basically fulfilling my needs, and I had already started to use it on my workstation[^1]. The project -sat there for a while, until I rediscovered this thing called *holidays*. +sat there for a while until I rediscovered this thing called *holidays*. [^1]: I tried so you do not have to: having my graphical session going crazy during a work meeting because of a software I had written. @@ -23,16 +23,16 @@ sat there for a while, until I rediscovered this thing called *holidays*. For a short week, I tried to address at many of the remaining issues and missing features that I was aware of. Then, I started to write [man pages](https://lthms.github.io/spatial-shell/spatial.1.html), which -turned out to be the perfect opportunity to clean-up every clunkiness I could -possibly found. +turned out to be the perfect opportunity to clean up every clunkiness I could +possibly find. -I can’t help but finding the result rather nice and satisfying, and I hope you +I can’t help but find the result rather nice and satisfying, and I hope you will enjoy it too! [Spatial Shell](https://github.com/lthms/spatial-shell) works on my machine, which means it will definitely break on yours. But this is where the fun lies, right? At this point, I definitely think the project is ready to fall into the hands of (motivated) alpha testers. -Anyway, let me give a tour! +Anyway, let me give you a tour! ## Spatial Model @@ -44,7 +44,7 @@ Shell can use two layouts: - **Maximize:** One window is displayed at a time - **Column:** Several windows are displayed side by side, to your convenience -The reason why **Maximize** is not a particular case of **Column**, but instead a +The reason **Maximize** is not a particular case of **Column**, but instead a layout on its own, is to easily allow you to switch to and back from maximizing the focused window. The following picture[^2] summarizes one particular setup with tree workspaces, each configured differently. @@ -54,7 +54,7 @@ tree workspaces, each configured differently. #[Spatial Shell allows users to configure the layout of each workspace individually.](/img/spatial-shell-example.png) - Workspace 1 contains three windows, and uses the **Column** layout to display - at most three windows, so every windows are visible, with the focus being on + at most three windows, so each window is visible, with the focus being on the leftmost one. - Workspace 2 contains four windows, and uses the **Column** layout to display at most two windows. As a consequence, two windows are not visible. @@ -81,7 +81,7 @@ More precisely, Spatial Shell comprises two executables: - [**spatialmsg**(1)](https://lthms.github.io/spatial-shell/spatialmsg.1.html), a client used to control the current instance of spatial. -Assuming `$spatial`{.bash} and `$spatialmsg`{.bash} contains the pathes to +Assuming `$spatial`{.bash} and `$spatialmsg`{.bash} contains the paths to spatial and spatialmsg binaries respectively, then the simplest sway configuration to start using Spatial Shell is the following @@ -131,9 +131,9 @@ unfocus opacity 85 See [**spatial**(5)](https://lthms.github.io/spatial-shell/spatial.5.html) for the list of commands supported by Spatial Shell. -As a sidenote, readers familiar with sway will definetely pick the resemblance +As a side note, readers familiar with sway will definitely pick the resemblance with sway and swaymsg, and it actually goes pretty deep. In a nutshell, swaymsg -connects to a UNIX socket created by sway at startup time, to sends it commands +connects to a UNIX socket created by sway at startup time, to send it commands (see [**spatial**(5)](https://lthms.github.io/spatial-shell/spatial.5.html)) using a dedicated IPC protocol inherited from i3 (see [**sway-ipc**(7)](https://lthms.github.io/spatial-shell/sway-ipc.7.html)). Not @@ -145,7 +145,7 @@ protocol ## Waybar Integration It is a common practice to use a so-called “bar” with sway, to display some -useful information about the current state of the system. In the `contrib/` +useful information about the current state of the system. In the `contrib/` directory of [Spatial Shell repository](https://github.com/lthms/spatial-shell), interested readers will find a configuration for [Waybar](https://github.com/Alexays/Waybar)[^design]. This configuration is diff --git a/site/posts/CleopatraV1.md b/site/posts/CleopatraV1.md index 55a850a..ddefcc0 100644 --- a/site/posts/CleopatraV1.md +++ b/site/posts/CleopatraV1.md @@ -11,16 +11,16 @@ abstract: | # A Literate Toolchain To Build This Website A literate program is a particular type of software program where code is not -directly written in source files, but rather in text document as code +directly written in source files, but rather in a text document as code snippets. In essence, literate programming allows for writing in the same place both the software program and its technical documentation. **`cleopatra`** is a “literate toolchain” I have implemented to build this website, and you are currently reading it[^past]. That is, **`cleopatra`** is -both the build system and an article of this website! To acheive this, +both the build system and an article of this website! To achieve this, **`cleopatra`** has been written as a collection of org files which can be either “tangled” using [Babel](https://orgmode.org/worg/org-contrib/babel/) or -“exported” as a HTML document. Tangling here refers to extracted marked code +“exported” as a HTML document. Tangling here refers to extract marked code blocks into files. [^past]: This sentence was true when this article was published, but things @@ -37,7 +37,7 @@ blocks into files. Because I have too much free time, probably. The page you are currently reading is **`cleopatra`** entry point. Its -primilarly purpose is to define two Makefiles —`makefile` and `bootstrap.mk`— +primary purpose is to define two Makefiles —`makefile` and `bootstrap.mk`— and the necessary emacs-lisp script to tangle this document. On the one hand, `makefile` is the main entrypoint of **`cleopatra`**. It @@ -51,9 +51,9 @@ On the other hand, `bootstrap.mk` is used to declare the various “generation processes” used to generate this website. `makefile` and the emacs-lisp scripts are versioned, because they are necessary -to bootstrap **`cleopatra`**; but since they are also define in this document, +to bootstrap **`cleopatra`**; but since they are also defined in this document, it means **`cleopatra`** can update itself, in some sense. This is to be kept in mind -when modifying this document to hastly. +when modifying this document to hastily. ## Global Constants and Variables @@ -107,7 +107,7 @@ cleanall : clean ``` Generation processes can declare new build outputs using the `+=` assignement -operators. Using another operator will likely provent an underisable result. +operators. Using another operator will likely provoke an undesirable result. ## Tangling Org Documents @@ -233,7 +233,7 @@ precisely, a generation process `proc` is defined in `proc.mk`. The rules of `proc-prebuild` for the `prebuild` stage. Eventually, the following dependencies are expected between within the chain of -generation processes for every generation processes. +generation processes for every generation process. ```makefile prebuild : proc-prebuild @@ -255,7 +255,7 @@ regarding the `include` directive. If there exists a rule to generate a Makefile used as an operand of `include`, `make` will use this rule to update (if necessary) said Makefile before actually including it. -Therefore, rules of the following form achieve our ambition of extensibility. +Therefore, the rules of the following form achieve our ambition of extensibility. ```makefile include ${PROC}.mk @@ -359,7 +359,7 @@ the current approach is 2. To modify `style/main.sass` in `theme` to import this file -Eventually, the second step will be automated, but in the meantime +Eventually, the second step will be automated, but, in the meantime, this customization is mandatory. ### Configuring Soupault @@ -392,7 +392,7 @@ In the present website, contents can be written in the following format: - **HTML Files:** This requires no particular set-up, since HTML is the *lingua franca* of `soupault`. -- **Regular Coq files:** Coq is a system which allows to write machine-checked +- **Regular Coq files:** Coq is a system which allows writing machine-checked proofs, and it comes with a source “prettifier” called `coqdoc`. [Learn more about the generation process for Coq files](https://src.soap.coffee/soap.coffee/lthms.git/tree/site/cleopatra/Contents/Coq.org?id=9329e9883a52eb95c0803a46560c396d149ef2c6). diff --git a/site/posts/ClightIntroduction.md b/site/posts/ClightIntroduction.md index 6598316..67b40db 100644 --- a/site/posts/ClightIntroduction.md +++ b/site/posts/ClightIntroduction.md @@ -83,13 +83,13 @@ Identifiers in Clight are (`positive`{.coq}) indices. The `fn_body` field is of type `statement`{.coq}, with the particular constructor `Sreturn`{.coq} whose argument is of type `option expr`{.coq}, and `statement`{.coq} and `expr`{.coq} look like the two main types to study. The predicates `step1`{.coq} and `step2`{.coq} allow for reasoning -about the execution of a `function`{.coq}, step by step (hence the name). It +about the execution of a `function`{.coq}, step-by-step (hence the name). It appears that `clightgen` generates Clight terms using the function call convention encoded by `step2`{.coq}. To reason about a complete execution, it appears that we can use `star`{.coq} (from the `Smallstep`{.coq} module) which is basically a trace of `step`{.coq}. These semantics are defined as predicates (that is, they live in `Prop`{.coq}). They allow for reasoning about -state-transformation, where a state is either +state transformation, where a state is either - A function call, with a given list of arguments and a continuation - A function return, with a result and a continuation @@ -325,7 +325,7 @@ familiar: `smart_inv`{.coq}, then renaming, etc. ``` We are almost done. Let’s simplify as much as possible `fetch_x`{.coq} and -`fetch_y`{.coq}. Each time, the `smart_inv`{.coq} tactic generates two suboals, +`fetch_y`{.coq}. Each time, the `smart_inv`{.coq} tactic generates two subgoals, but only the first one is relevant. The second one is not, and can be discarded. @@ -379,7 +379,7 @@ The definitions of Clight are straightforward, and the [CompCert documentation](http://compcert.inria.fr/doc/index.html) is very pleasant to read. Understanding Clight and its semantics can be very interesting if you are working on a language that you want to translate into machine code. -However, proving functional properties of a given C snippet using only CompCert +However, proving some functional properties of a given C snippet using only CompCert can quickly become cumbersome. From this perspective, the [VST](https://github.com/PrincetonUniversity/VST) project is very interesting, as its main purpose is to provide tools to reason about Clight programs more diff --git a/site/posts/ColorlessThemes-0.2.md b/site/posts/ColorlessThemes-0.2.md index 625b604..8cb32a4 100644 --- a/site/posts/ColorlessThemes-0.2.md +++ b/site/posts/ColorlessThemes-0.2.md @@ -22,7 +22,7 @@ relying on the presence of these functions to decide whether a file provides a theme or not. As of now, `nordless-theme` and `lavenderless-theme` have been updated accordingly, and [they appear on Peach Melpa](https://peach-melpa.org/themes/lavenderless-theme/variants/lavenderless). -Their loading can also be defered using the `:defer`{.lisp} keyword of the +Their loading can also be deferred using the `:defer`{.lisp} keyword of the `use-package`{.lisp} macro. if you happen to be a user of `colorless-themes`, feel free to shoot an email! diff --git a/site/posts/Coqffi-1-0-0.md b/site/posts/Coqffi-1-0-0.md index e8fce8c..e90d5b5 100644 --- a/site/posts/Coqffi-1-0-0.md +++ b/site/posts/Coqffi-1-0-0.md @@ -65,7 +65,7 @@ in a less direct manner. `coqffi` supports a set of primitive types, *i.e.*, a set of OCaml types for which it knows an equivalent type in Coq. The list is the following (the Coq types are fully qualified in the table, but not in -the generated Coq module as the necessary `Import` statement are +the generated Coq module as the necessary `Import` statements are generated too). | OCaml type | Coq type | @@ -87,7 +87,7 @@ signed primitive integers to Coq users. They are implemented on top of the deprecated once the support for [signed primitive integers](https://github.com/coq/coq/pull/13559) is implemented[^compat]. -[^compat]: This is actually one of the sources of incompatibilities of `coqffi` +[^compat]: This is actually one of the sources of incompatibility of `coqffi` with most recent versions of Coq. When processing the entries of a given interface model, `coqffi` will @@ -157,7 +157,7 @@ Polymorphism is supported, *i.e.*, `type 'a t`{.ocaml} becomes `Axiom t : forall (a : Type), Type`{.coq}. It is possible to provide a “model” for a type using the `coq_model` -annotation, for instance for reasoning purposes. For instance, we can specify +annotation, for instance, for reasoning purposes. That is, we can specify that a type is equivalent to a `list`. ```ocaml @@ -174,7 +174,7 @@ It is important to be careful when using the =coq_model= annotation. More precisely, the fact that `t` is a `list` in the “Coq universe” shall not be used while the implementation phase, only the verification phase. -Unamed polymorphic type parameters are also supported. In presence of +Unnamed polymorphic type parameters are also supported. In presence of such parameters, `coqffi` will find it a name that is not already used. For instance, @@ -190,7 +190,7 @@ Axiom ast : forall (b : Type) (a : Type), Type. Finally, `coqffi` has got an experimental feature called `transparent-types` (enabled by using the `-ftransparent-types` command-line argument). If the type -definition is given in the module interface, then `coqffi` tries to generates +definition is given in the module interface, then `coqffi` tries to generate an equivalent definition in Coq. For instance, ```ocaml @@ -236,7 +236,7 @@ is satisfied. ### Pure values -`coqffi` decides whether or not a given OCaml values is pure or impure +`coqffi` decides whether or not a given OCaml value is pure or impure with the following heuristics: - Constants are pure @@ -247,7 +247,7 @@ with the following heuristics: functions (which do not live inside the [~Lwt~](https://ocsigen.org/lwt/5.3.0/manual/manual) monad) are pure -Similarly to types, `coqffi` generates axioms (or definitions, if the +Similarly to types, `coqffi` generates axioms (or definitions if the `coq_model` annotation is used) for pure values. Then, ```ocaml @@ -272,7 +272,7 @@ becomes Axiom map : forall (a : Type) (b : Type), (a -> b) -> list a -> list b. ``` -Again, unamed polymorphic type are supported, so +Again, unnamed polymorphic typse are supported, so ```ocaml val ast_to_string : _ ast -> string [@@pure] @@ -400,7 +400,7 @@ Definition console_unsafe_semantics : semantics CONSOLE := primitives —*i.e.*, functions which live inside the `Lwt` monad— when the `lwt` feature is enabled. -The treatment is very analoguous to the one for impure primitives: (1) +The treatment is very analogous to the one for impure primitives: (1) a typeclass is generated (with the `_Async` suffix), and (2) an instance for the `Lwt` monad is generated. Besides, an instance for the “synchronous” primitives is also generated for `Lwt`. If the @@ -418,7 +418,7 @@ you are using an alias type in place of `Lwt.t`. OCaml features an exception mechanism. Developers can define their own exceptions using the `exception` keyword, whose syntax is similar -to constructors definition. For instance, +to the constructors’ definition. For instance, ```ocaml exception Foo of int * bool @@ -427,7 +427,7 @@ exception Foo of int * bool introduces a new exception `Foo` which takes two parameters of type `int`{.ocaml} and `bool`{.ocaml}. `Foo (x, y)` constructs of value of type `exn`{.ocaml}. -For each new exceptions introduced in an OCaml module, `coqffi` +For each new exception introduced in an OCaml module, `coqffi` generates (1) a so-called “proxy type,” and (2) conversion functions to and from this type. @@ -462,7 +462,7 @@ and how `coqffi` supports it will probably be generalized in future releases. Finally, `coqffi` has a minimal support for functions which may raise exceptions. Since OCaml type system does not allow to identify such -functions, they need to be annotated explicitely, using the +functions, they need to be annotated explicitly, using the =may_raise= annotation. In such a case, `coqffi` will change the return type of the function to use the =sum= Coq inductive type. @@ -481,7 +481,7 @@ Axiom from_option : forall (a : Type), option a -> sum a exn. ### Modules Lastly, `coqffi` supports OCaml modules described within `mli` files, -when they are specify as `module T : sig ... end`{.ocaml}. For instance, +when they are specified as `module T : sig ... end`{.ocaml}. For instance, ```ocaml module T : sig diff --git a/site/posts/CoqffiEcho.md b/site/posts/CoqffiEcho.md index 3dc87c9..0494854 100644 --- a/site/posts/CoqffiEcho.md +++ b/site/posts/CoqffiEcho.md @@ -58,7 +58,7 @@ stanzas like `coq.theory` and `coq.extraction`. The following graph summarizes the dependencies between each component (plain arrows symbolize software dependencies). -#[The echo server dependency graph. Dashed boxes are generated.](/img/echo-deps.svg) +#[The echo server dependency graph. Dashed boxes are generated.](/img/echo-deps.svg [The echo server dependy graph]) We enable Coq-related stanza with `(using coq 0.2)`{.lisp} in the `dune-project`{.dune}. file. diff --git a/site/posts/DiscoveringCommonLisp.md b/site/posts/DiscoveringCommonLisp.md index a947110..b3c1e3d 100644 --- a/site/posts/DiscoveringCommonLisp.md +++ b/site/posts/DiscoveringCommonLisp.md @@ -14,7 +14,7 @@ I always wanted to learn some Lisp dialect. In the meantime, take shape. So, of course, my brain got an idea: *why not writing a client for lykan in some Lisp dialect?*[^why] I asked on [Mastodon](https://mastodon.social/@lthms/100135240390747697) if there were -good game engine for Lisp, and someone told me about +good game engines for Lisp, and someone told me about [`trivial-gamekit`](https://github.com/borodust/trivial-gamekit). [^why]: Spoiler alert: this wasn’t the most efficient approach for the lykan @@ -36,9 +36,9 @@ requirements. Two are related to Lisp: 2. SBCL or CCL [Quicklisp](https://quicklisp.org/beta) is an experimental package manager for -Lisp project, while SBCL and CCL are two Lisp implementations. I had already +Lisp projects, while SBCL and CCL are two Lisp implementations. I had already installed [Clisp](https://www.archlinux.org/packages/?name=clisp), and it took -me quite some times to understand my mistake. Fortunately, +me quite some time to understand my mistake. Fortunately, [SBCL](https://www.archlinux.org/packages/?name=sbcl) is also packaged in ArchLinux. @@ -50,7 +50,7 @@ the process, you will have a new directory `${HOME}/quicklisp`{.bash}[^go]. workspace](https://github.com/golang/go/wiki/SettingGOPATH). Quicklisp is not a native feature of SBCL, and requires a small bit of -configuration to be made available automatically. You have to create a file +configurations to be made available automatically. You have to create a file `${HOME}/.sbclrc`{.bash}, with the following content: ```lisp @@ -127,18 +127,18 @@ Basically, this means we use two symbols, `run`{.lisp} and `app`{.lisp}. ### A Game Client The `lysk.lisp` file contains the program in itself. My first goal was to -obtain the following program: at startup, it shall creates a new window in +obtain the following program: at startup, it shall create a new window in fullscreen, and exit when users release the left button of their mouse. It is worth mentioning that I had to report [an issue to the `trivial-gamekit` upstream](https://github.com/borodust/trivial-gamekit/issues/30) in order to make my program work as expected. -While it may sounds scary —it suggests `trivial-gamekit` is a relatively young +While it may sound scary —it suggests `trivial-gamekit` is a relatively young project— the author has implemented a fix in less than an hour! He also took the time to answer many questions I had when I joined the `#lispgames` Freenode channel. -Before going any further, lets have a look at the complete file. +Before going any further, let’s have a look at the complete file. ```lisp (cl:in-package :lysk) @@ -177,10 +177,10 @@ sbcl --eval '(ql:quickload :lysk)' --eval '(lysk:run)' It looks like empower a REPL-driven development. That being said, once the development is finished, I don't think I will have a lot of success if I ask my -future players to start sbcl to enjoy my game. Fortunately, `trivial-gamekit` +future players to start SBCL to enjoy my game. Fortunately, `trivial-gamekit` provides a dedicated function to bundle the game as a standalone executable. -Following the advises of the [**@borodust**](https://github.com/borodust) —the +Following the advice of the [**@borodust**](https://github.com/borodust) —the `trivial-gamekit` author— I created a second package to that end. First, we need to edit the `lysk.asd` file to detail a second package: @@ -223,7 +223,7 @@ sbcl --eval "(ql:quickload :lysk/bundle)" \ Objectively, there is not much in this article. However, because I am totally new to Lisp, it took me quite some time to get these few lines of code to work together. All being told I think this constitutes a good `trivial-gamekit` -skeleton. Do not hesitate to us it this way. +skeleton. Do not hesitate to use it this way. Thanks again to [**@borodust**](https://github.com/borodust), for your time and all your answers! diff --git a/site/posts/EndOfPhd.md b/site/posts/EndOfPhd.md index 0b5a445..7299450 100644 --- a/site/posts/EndOfPhd.md +++ b/site/posts/EndOfPhd.md @@ -56,13 +56,13 @@ Our contribution is two-fold: verification of complex systems made of interconnected components as a first step towards addressing the challenge posed by the scale of the x86 hardware architecture. This approach is not specific to hardware models, and could - also be leveraged to reason about composition of software components as + also be leveraged to reason about the composition of software components as well. In addition, we have implemented our approach in the Coq theorem - prover, and the resulting framework takes advantages of Coq proof automation + prover, and the resulting framework takes advantage of Coq proof automation features to provide general-purpose facilities to reason about components interactions. -## Publicatinos +## Publications If you are interested, you can have a look at the paper I wrote during my PhD: @@ -78,4 +78,3 @@ You can also have a look at the Coq frameworks I have published: - [SpecCert on Github](https://github.com/lthms/speccert) (CeCILL-B) - [FreeSpec on Github](https://github.com/lthms/FreeSpec) (MPL-2.0) - diff --git a/site/posts/ExtensibleTypeSafeErrorHandling.md b/site/posts/ExtensibleTypeSafeErrorHandling.md index 7e6e747..216a185 100644 --- a/site/posts/ExtensibleTypeSafeErrorHandling.md +++ b/site/posts/ExtensibleTypeSafeErrorHandling.md @@ -27,7 +27,7 @@ which may print to and read from the standard output. A function `askPassword`{.haskell} which displays a prompt and get the user password would have this type signature: -[^fm2018]: The odds were in my favour: the aforementioned academic article has +[^fm2018]: The odds were in my favor: the aforementioned academic article has been accepted. ```haskell @@ -42,7 +42,7 @@ become burdensome to use. Basically, when my colleague showed me his Rust project and how he was using `error-chain`, the question popped out. *Can we use an approach similar to -`Eff`{.haskell} to implement a Haskell-flavoured `error-chain`?* +`Eff`{.haskell} to implement a Haskell-flavored `error-chain`?* Spoiler alert: the answer is yes. In this post, I will dive into the resulting API, leaving for another time the details of the underlying implementation[^api]. @@ -131,13 +131,13 @@ for the latter, the current implementation of `ResultT`{.haskell} is probably less powerful, but to be honest I mostly cared about the “extensible” thing, so it is not very surprising. -This monad is not an alternative to neither Monad Stacks a la mtl nor to the +This monad is an alternative to neither Monad Stacks a la mtl nor to the `Eff`{.haskell} monad. In its current state, it aims to be a more powerful and flexible version of `EitherT`{.haskell}. ### Parameters -As often in Haskell, the `ResultT`{.haskell} monad can be parameterised in +As often in Haskell, the `ResultT`{.haskell} monad can be parameterized in several ways. ```haskell @@ -152,7 +152,7 @@ data ResultT msg (err :: [*]) m a `ResultT`{.haskell} is not intended to be stacked itself - `a`{.haskell} is the expected type of the computation result -[^row]: You might have notice `err`{.haskell} is of kind `[*]`{.haskell}. To write such a thing, +[^row]: You might have noticed `err`{.haskell} is of kind `[*]`{.haskell}. To write such a thing, you will need the [`DataKinds`{.haskell}](https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell) GHC pragmas. @@ -197,7 +197,7 @@ readContent :: (Contains err FileError, MonadIO m) -> ResultT msg err m String ``` -We could leverage this function in a given project, for instance to read its +We could leverage this function in a given project, for instance, to read its configuration files (for the sake of the example, it has several configuration files). This function can use its own type to describe ill-formed description (`ConfigurationError`{.haskell}). @@ -277,7 +277,7 @@ row of errors, by providing as many functions as required. Finally, only one function tied to a given typeclass, on the condition that the handling errors implement this typeclass. -Using `recover`{.haskell} and its siblings often requires to help a bit the +Using `recover`{.haskell} and its siblings often require to help a bit the Haskell type system, especially if we use lambdas to define the error handlers. Doing that is usually achieved with the `Proxy a`{.haskell} dataype (where `a`{.haskell} is a phantom type). I would rather use the @@ -300,7 +300,7 @@ use more errors thanks to the `recover*` functions. [^tap]: The [TypeApplications](https://medium.com/@zyxoas/abusing-haskell-dependent-types-to-make-redis-queues-safer-cc31db943b6c) - pragmas is probably one of my favourites. + pragmas is probably one of my favorites. When I use it, it feels almost like if I were writing a Coq document. @@ -309,7 +309,7 @@ use more errors thanks to the `recover*` functions. `ResultT`{.haskell} only cares about error handling. The rest of the work is up to the underlying monad `m`{.haskell}. That being said, nothing forbids us to provide fine-grained API, *e.g.*, for Filesystem-related functions. From an -error handling perspective, the functions provided by Prelude (the standard +error handling perspective, the functions provided by `Prelude` (the standard library of Haskell) are pretty poor, and the documentation is not really precise regarding the kind of error we can encounter while using it. diff --git a/site/posts/LtacMetaprogramming.md b/site/posts/LtacMetaprogramming.md index b98692e..2f3e6d7 100644 --- a/site/posts/LtacMetaprogramming.md +++ b/site/posts/LtacMetaprogramming.md @@ -22,12 +22,12 @@ logical reasoning. For instance, to reason by induction, one can use the `destruct`{.coq} or `case_eq`{.coq} tactics, etc. It is not uncommon for new Coq users to be introduced to Ltac, the Coq default tactic language, using this proof-centric approach. This is not surprising, since writing proofs remains -the main use-case for Ltac. In practice though, this discourse remains an +the main use case for Ltac. In practice, though, this discourse remains an abstraction which hides away what actually happens under the hood when Coq -executes a proof scripts. +executes a proof script. To really understand what Ltac is about, we need to recall ourselves that -Coq kernel is mostly a typechecker. A theorem statement is expressed as a +Coq kernel is mostly a type checker. A theorem statement is expressed as a “type” (which lives in a dedicated sort called `Prop`{.coq}), and a proof of this theorem is a term of this type, just like the term `S (S O)`{.coq} ($2$) is of type `nat`{.coq}. Proving a theorem in Coq requires to construct a term @@ -62,7 +62,7 @@ tactic has been used, the term we are trying to construct consists solely in a hole, while Coq presents us a goal with no hypothesis, and with the exact type of our theorem, that is `forall (n : nat), n + O = n`{.coq}. -A typical Coq course will explain students the `intro`{.coq} tactic allows for +A typical Coq course will explain to students the `intro`{.coq} tactic allows for turning the premise of an implication into an hypothesis within the context. $$C \vdash P \rightarrow Q$$ @@ -72,7 +72,7 @@ becomes $$C,\ P \vdash Q$$ This is a fundamental rule of deductive reasoning, and `intro`{.coq} encodes it. -It achieves this by refining the current hole into an anymous function. +It achieves this by refining the current hole into an anonymous function. When we use ```coq @@ -91,7 +91,7 @@ into fun (n : nat) => ?Goal2 ``` -The next step of this proof is to reason about induction on [n]. For [nat], +The next step of this proof is to reason about induction on `n`. For `nat`, it means that to be able to prove $$\forall n, \mathrm{P}\ n$$ @@ -174,7 +174,7 @@ Inductive eq (A : Type) (x : A) : A -> Prop := Coming back to our current goal, proving `@eq nat (Nat.add 0 0) 0`{.coq}[^equ1] requires to construct a term of a type whose only constructor is `eq_refl`{.coq}. `eq_refl`{.coq} accepts one argument, and encodes the proof -that said argument is equal to itself. In practice, Coq typechecker will accept +that said argument is equal to itself. In practice, Coq type checker will accept the term `@eq_refl _ x`{.coq} when it expects a term of type `@eq _ x y`{.coq} *if* it can reduce `x`{.coq} and `y`{.coq} to the same term. @@ -217,7 +217,7 @@ the same term. However, at this point of the proof, we have the `IHn`{.coq} hypothesis (*i.e.*, the `IHn`{.coq} argument of the anonymous function whose body we are trying to construct). The `rewrite`{.coq} tactic allows for substituting in a type an -occurence of `x`{.coq} by `y`{.coq} as long as we have a proof of `x = y`{.coq}. *) +occurrence of `x`{.coq} by `y`{.coq} as long as we have a proof of `x = y`{.coq}. *) ```coq rewrite IHn. @@ -247,10 +247,10 @@ the proof term that we have carefully constructed. n) ``` -We can finally use `Qed`{.coq} or `Defined`{.coq} to tell Coq to typecheck this -term. That is, Coq does not trust Ltac, but rather typecheck the term to +We can finally use `Qed`{.coq} or `Defined`{.coq} to tell Coq to type check this +term. That is, Coq does not trust Ltac, but rather type check the term to verify it is correct. This way, in case Ltac has a bug which makes it -construct ill-formed type, at the very least Coq can reject it. +construct an ill-formed type, at the very least Coq can reject it. ```coq Qed. @@ -258,7 +258,7 @@ Qed. In conclusion, tactics are used to incrementally refine hole inside a term until the latter is complete. They do it in a very specific manner, to -encode certain reasoning rule. +encode certain reasoning rules. On the other hand, the `refine`{.coq} tactic provides a generic, low-level way to do the same thing. Knowing how a given tactic works allows for mimicking diff --git a/site/posts/LtacPatternMatching.md b/site/posts/LtacPatternMatching.md index 9cc926e..2210a61 100644 --- a/site/posts/LtacPatternMatching.md +++ b/site/posts/LtacPatternMatching.md @@ -20,7 +20,7 @@ In the [a previous article](/posts/LtacMetaprogramming.html) of our series on Ltac, we have shown how tactics allow for constructing Coq terms incrementally. Ltac programs (“proof scripts”) generate terms, and the shape of said terms can be very different regarding the initial context. For instance, `induction -x`{.coq} will refine the current goal using an inductive principle dedicated to +x`{.coq} will refine the current goal by using an inductive principle dedicated to the type of `x`{.coq}. This is possible because Ltac allows for pattern matching on types and @@ -38,7 +38,7 @@ Ltac is not a total language: a tactic may not always succeed. Ltac programmers can use `match`{.coq} or `lazymatch`{.coq}. One the one hand, with `match`{.coq}, if one pattern matches, but the branch body fails, Coq will backtrack and try the next branch. On the other hand, `lazymatch`{.coq} will -stop on error. +stop with an error. So, for instance, the two following tactics will print two different messages: @@ -93,7 +93,7 @@ Ltac successive x y := end. ``` -`successive x y`{.coq} will fails if `y`{.coq} is not the successor of +`successive x y`{.coq} will fail if `y`{.coq} is not the successor of `x`{.coq}. On the contrary, the “syntactically equivalent” function in Gallina will exhibit a totally different behavior. @@ -184,20 +184,20 @@ With `goal`{.coq}, patterns are of the form `H : (pattern), ... |- (pattern)`{.coq}. - At the left side of `|-`{.coq}, we match on hypotheses. Beware that - contrary to variable name in pattern, hypothesis names behaves as in + contrary to variable names in pattern, hypothesis names behaves as in Gallina (i.e., fresh binding, shadowing, etc.). In the branch, we are - looking for equations, i.e., an hypothesis of the form `?x = _`{.coq}. + looking for equations, i.e., a hypothesis of the form `?x = _`{.coq}. - At the right side of `|-`{.coq}, we match on the goal. In both cases, Ltac makes available an interesting operator, -`context[(pattern)`{.coq}], which is satisfies if `(pattern)`{.coq} appears somewhere in +`context[(pattern)`{.coq}], which is satisfied if `(pattern)`{.coq} appears somewhere in the object we are pattern matching against. So, the branch of the `match`{.coq} reads as follows: we are looking for an equation `H`{.coq} which specifies the value of an object `x`{.coq} which appears in the goal. If such an equation -exists, `subst'`{.coq} tries to `rewrite x`{.coq} as many time as possible. +exists, `subst'`{.coq} tries to `rewrite x`{.coq} as many times as possible. This implementation of `subst'`{.coq} is very fragile, and will not work if the -equation is of the form `_ = ?x`{.coq}, and it may behaves poorly if we have +equation is of the form `_ = ?x`{.coq}, and it may behave poorly if we have “transitive equations”, such as there exists hypotheses `?x = ?y`{.coq} and `?y -= _`{.coq}. Motivated readers may be interested in proposing more robust += _`{.coq}. Motivated readers may be interested in proposing a more robust implementation of `subst'`{.coq}. diff --git a/site/posts/MixingLtacAndGallina.md b/site/posts/MixingLtacAndGallina.md index f03e7e3..288f38f 100644 --- a/site/posts/MixingLtacAndGallina.md +++ b/site/posts/MixingLtacAndGallina.md @@ -15,14 +15,14 @@ abstract: | # Mixing Ltac and Gallina for Fun and Profit -One of the most misleading introduction to Coq is to say that “Gallina is +One of the most misleading introductions to Coq is to say that “Gallina is for programs, while tactics are for proofs.” Indeed, in Coq we construct terms of given types, always. Terms encodes both programs and proofs about these programs. Gallina is the preferred way to construct programs, and tactics are the preferred way to construct proofs. The key word here is “preferred.” We do not always need to use tactics to -construct a proof term. Conversly, there are some occasions where +construct a proof term. Conversely, there are some occasions where constructing a program with tactics become handy. Furthermore, Coq actually allows for *mixing together* Ltac and Gallina. @@ -38,10 +38,10 @@ metaprogramming (that is, the generation of programs by programs). ## A Tale of Two Worlds, and Some Bridges Constructing terms proofs directly in Gallina often happens when one is -writing dependently-typed definition. For instance, we can write a type safe +writing dependently typed definition. For instance, we can write a type-safe `from_option`{.coq} function (inspired by [this very nice write-up](https://plv.csail.mit.edu/blog/unwrapping-options.html)) such that -the option to unwrap shall be accompagnied by a proof that said option contains +the option to unwrap shall be accompanied by a proof that said option contains something. This extra argument is used in the `None`{.coq} case to derive a proof of `False`{.coq}, from which we can derive anything. @@ -87,7 +87,7 @@ Proof. Defined. ``` -There is a third approach we can consider: mixing Gallina terms, and tactics. +There is a third approach we can consider: mixing Gallina terms and tactics. This is possible thanks to the `ltac:()`{.coq} feature. ```coq @@ -104,8 +104,8 @@ Definition from_option'' {α} When Coq encounters `ltac:()`{.coq}, it treats it as a hole. It sets up a corresponding goal, and tries to solve it with the supplied tactic. -Conversly, there exists ways to construct terms in Gallina when writing a proof -script. Certains tactics takes such terms as arguments. Besides, Ltac provides +Conversely, there exists ways to construct terms in Gallina when writing a proof +script. Certain tactics take such terms as arguments. Besides, Ltac provides `constr:()`{.coq} and `uconstr:()`{.coq} which work similarly to `ltac:()`{.coq}. The difference between `constr:()`{.coq} and `uconstr:()`{.coq} is that Coq will try to assign a type to the argument of @@ -122,7 +122,7 @@ Tactic Notation "wrap_id" uconstr(x) := Both `x`{.coq} the argument of `wrap_id`{.coq} and `f`{.coq} the anonymous identity function are not typed. It is only when they are composed together as an argument of `exact`{.coq} (which expects a typed argument, more precisely of the type of the -goal) that Coq actually tries to typecheck it. +goal) that Coq actually tries to type check it. As a consequence, `wrap_id`{.coq} generates a specialized identity function for each specific context. @@ -145,7 +145,7 @@ Besides, we do not need to give more type information about `nil`{.coq}. If ## Beware the Automation Elephant in the Room Proofs and computational programs are encoded in Coq as terms, but there is a -fundamental difference between them, and it is highlighted by one of the axiom +fundamental difference between them, and it is highlighted by one of the axioms provided by the Coq standard library: proof irrelevance. Proof irrelevance states that two proofs of the same theorem (i.e., two proof @@ -176,11 +176,12 @@ add = fun _ y : nat => y That being said, if we keep that in mind, and assert the correctness of the generated programs (either by providing a proof, or by extensively testing it), there is no particular reason not to use Ltac to generate terms when it makes -sens. +sense. -Dependently-typed programming can help here. If we decorate the return type of +Dependently typed programming can help you here. If we decorate the return type of a function with the expected properties of the result wrt. the function’s -arguments, we can ensure the function is correct, and conversly prevent tactics +arguments, we can ensure the function is correct, and conversely prevent tactics such as `auto`{.coq} to generate “incorrect” terms. Interested readers may refer to [the dedicated series on this very website](/posts/StronglySpecifiedFunctions.html). + diff --git a/site/posts/MonadTransformers.md b/site/posts/MonadTransformers.md index 6f1d5aa..9b9f2a8 100644 --- a/site/posts/MonadTransformers.md +++ b/site/posts/MonadTransformers.md @@ -23,14 +23,14 @@ in Rust or Elixir, but it works great in Haskell. Unfortunately, it is not an easy concept and it can be hard to understand. This article is not an attempt to do so, but rather a postmortem review of one situation where I found them extremely useful. If you think you have understood how they work, but don’t see -the point yet, you might find here a beginning of answer. +the point yet, you might find here a beginning of the answer. Recently, I ran into a very good example of why Monad Transformers worth it[^doubts]. I have been working on a project called ogma for a couple years now. In a nutshell, I want to build “a tool” to visualize in time and space a -storytelling. We are not here just yet, but in the meantime I have wrote a +storytelling. We are not here just yet, but, in the meantime, I have written a software called `celtchar` to build a novel from a list of files. One of its -newest feature is the choice of language, and by extension, the typographic +newest features is the choice of language, and by extension, the typographic rules. This information is read from a configuration file very early in the program flow. Unfortunately, its use comes much later, after several function calls. @@ -40,7 +40,7 @@ calls. Transformers are a great abstraction, but nowadays I would probably try to choose another approach. -In Haskell, you deal with that kind of challenges by relying on the Reader +In Haskell, you deal with that kind of challenge by relying on the Reader Monad. It carries an environment in a transparent way. The only thing is, I was already using the State Monad to carry the computation result. But that’s not an issue with the Monad Transformers. @@ -53,7 +53,7 @@ issue with the Monad Transformers. As you may have already understood, I wasn't using the “raw” `State`{.haskell} Monad, but rather the transformer version `StateT`{.haskell}. The underlying Monad was `IO`{.haskell}, because I needed to be able to read some files from -the filesystem. By replacing `IO`{.haskell} by `ReaderT Language IO`{.haskell}, +the file system. By replacing `IO`{.haskell} by `ReaderT Language IO`{.haskell}, I basically fixed my “carry the variable to the correct function call easily” problem. @@ -68,7 +68,7 @@ And that was basically it. Now, my point is not that Monad Transformers are the ultimate beast we will have to tame once and then everything will be shiny and easy[^funny]. There are a lot of -other way to achieve what I did with my `Builder`{.haskell} stack. For instance, in an +other ways to achieve what I did with my `Builder`{.haskell} stack. For instance, in an OO language, I probably would have to add a new class member to my `Builder`{.haskell} class and I would have done basically the same thing. @@ -76,8 +76,8 @@ class and I would have done basically the same thing. However, there is something I really like about this approach: the `Builder`{.haskell} type definition gives you a lot of useful information -already. Both the `State`{.haskell} and `Reader`{.haskell} Monads have a well -established semantics most Haskellers will understand in a glance. A bit of -documentation won’t hurt, but I suspect it is not as necessary as one could +already. Both the `State`{.haskell} and `Reader`{.haskell} Monads have a +well-established semantics most Haskellers will understand in a glance. A bit +of documentation won’t hurt, but I suspect it is not as necessary as one could expect. Moreover, the presence of the `IO`{.haskell} Monad tells everyone using the `Builder`{.haskell} Monad might cause I/O. diff --git a/site/posts/NeovimOCamlTreeSitterAndLSP.md b/site/posts/NeovimOCamlTreeSitterAndLSP.md index 9769d94..c61ece7 100644 --- a/site/posts/NeovimOCamlTreeSitterAndLSP.md +++ b/site/posts/NeovimOCamlTreeSitterAndLSP.md @@ -21,7 +21,7 @@ OCaml hacking and calling it a day. In a nutshell, OCaml `mli` files are quickly turning into a random mess of nonsensical colors, and I didn’t know why. I tried to blame [`tree-sitter-ocaml`](https://github.com/tree-sitter/tree-sitter-ocaml/issues/72), -but of course I was wrong. +but, of course I was wrong. The issue is subtle, and to be honest, I don’t know if I totally grasp it. But from my rough understanding, it breaks down as follows. diff --git a/site/posts/November2022.md b/site/posts/November2022.md index d35e0a9..6f7d5e5 100644 --- a/site/posts/November2022.md +++ b/site/posts/November2022.md @@ -32,7 +32,7 @@ Writing again was really nice, and I even gave writing fiction in English a shot. That made me uncover a bug in the English support of [ogam](https://crates.io/crates/ogam), my markup language for fiction writers, which led me to publish a fix on Crates.io. However, as soon as I came back to -`$WORK`{.bash}, my writing spree ended. That’s Okay, though. It gave me plenty +`$WORK`{.bash}, my writing spree ended. That’s okay, though. It gave me plenty of ideas for future sessions. Thanks, NaNoWriMo! Sorry to quit so soon, and see you next year, maybe. @@ -42,5 +42,5 @@ on adding proper support for `coqffi` to and Coq! I’m thrilled by this. Thanks, [**@Alizter**](https://github.com/Alizter)! -This wraps-up this retrospective. I hope I will have more interesting, +This wraps up this retrospective. I hope I will have more interesting, concrete news to share next month. diff --git a/site/posts/RankNTypesInOCaml.md b/site/posts/RankNTypesInOCaml.md index c133c69..d2021ce 100644 --- a/site/posts/RankNTypesInOCaml.md +++ b/site/posts/RankNTypesInOCaml.md @@ -27,9 +27,9 @@ Error: This expression has type b but an expression was expected of type a ``` -When OCaml tries to type-check `foo`{.ocaml}, it infers `id`{.ocaml} expects an +When OCaml tries to type check `foo`{.ocaml}, it infers `id`{.ocaml} expects an argument of type `a`{.ocaml} because of `id x`{.ocaml}, then fails when trying -to type-check `id y`{.ocaml}. +to type check `id y`{.ocaml}. The trick to be able to write `foo`{.ocaml} is to use records. Indeed, while the argument of a function cannot be polymorphic, the field of a record can. @@ -45,13 +45,13 @@ let foo {id} x y = (id x, id y) From a runtime perspective, it is possible to tell OCaml to remove the introduced indirection with the `unboxed`{.ocaml} annotation. There is nothing we can do in the source, though. We need to destruct `id`{.ocaml} in -`foo`{.ocaml}, and we need to construct it at its call-site. +`foo`{.ocaml}, and we need to construct it at its call site. ```ocaml g {id = fun x -> x} ``` As a consequence, this solution is not a silver bullet, but it is an option -that is worth considering if, *e.g.*, it allows to export a cleaner API to the +that is worth considering if, *e.g.*, it allows us to export a cleaner API to the consumer of a module. Personally, I have been considering this trick recently to remove the need for a library to be implemented as a functor. diff --git a/site/posts/RewritingInCoq.md b/site/posts/RewritingInCoq.md index e22f814..a0e65fb 100644 --- a/site/posts/RewritingInCoq.md +++ b/site/posts/RewritingInCoq.md @@ -14,7 +14,7 @@ secret, which takes the form of a set of unnecessary axioms. I thought I couldn’t avoid them at first, but it was before I heard about “generalized rewriting,” setoids and morphisms. Now, I know the truth, and I will have to update SpecCert eventually. But, in the meantime, let me try to -explain how it is possible to rewrite a term in a proof using a ad-hoc +explain how it is possible to rewrite a term in a proof using an ad hoc equivalence relation and, when necessary, a proper morphism. ## Case Study: Gate System @@ -35,7 +35,7 @@ Record Gate := According to this definition, a gate can be either open or closed. It can also be locked, but if it is, it cannot be open at the same time. To express this -constrain, we embed the appropriate proposition inside the Record. By doing so, +constraint, we embed the appropriate proposition inside the Record. By doing so, we *know* for sure that we will never meet an ill-formed `Gate`{.coq} instance. The Coq engine will prevent it, because to construct a gate, one will have to prove the `lock_is_close`{.coq} predicate holds. @@ -158,7 +158,7 @@ Definition gate_eq ``` Because “equality” means something very specific in Coq, we won't say “two -gates are equal” anymore, but “two gates are equivalent”. That is, +gates are equal” anymore, but “two gates are equivalent.” That is, `gate_eq`{.coq} is an equivalence relation. But “equivalence relation” is also something very specific. For instance, such relation needs to be symmetric (`R x y -> R y x`{.coq}), reflexive (`R x x`{.coq}) and transitive (`R x y -> R y z @@ -226,7 +226,7 @@ Qed. ## Equivalence Relations and Rewriting -So here we are, with our ad-hoc definition of gate equivalence. We can use +So here we are, with our ad hoc definition of gate equivalence. We can use `symmetry`{.coq}, `reflexivity`{.coq} and `transitivity`{.coq} along with `gate_eq`{.coq} and it works fine because we have told Coq `gate_eq`{.coq} is indeed an equivalence relation for `Gate`{.coq}. @@ -295,9 +295,9 @@ The `rewrite`{.coq} tactic works out of the box with the Coq equality `x`{.coq} and `y`{.coq} are equal iff every property on `A`{.coq} which is true of `x`{.coq} is also true of `y`{.coq} -This is a pretty strong property, and one a lot of equivalence relations do not +This is a pretty strong property, and one that a lot of equivalence relations do not have. Want an example? Consider the relation `R`{.coq} over `A`{.coq} such that -forall `x`{.coq} and `y`{.coq}, `R x y`{.coq} holds true. Such relation is +forall `x`{.coq} and `y`{.coq}, `R x y`{.coq} holds true. Such a relation is reflexive, symmetric and reflexive. Yet, there is very little chance that given a function `f : A -> B`{.coq} and `R’`{.coq} an equivalence relation over `B`{.coq}, `R x y -> R' (f x) (f y)`{.coq}. Only if we have this property, we diff --git a/site/posts/September2022.md b/site/posts/September2022.md index d004ded..2a15d25 100644 --- a/site/posts/September2022.md +++ b/site/posts/September2022.md @@ -20,11 +20,11 @@ step back and reflect of what happened these past few thirty days or so[^syntax]. [^syntax]: There is the shocking news that I have started to use syntax - highlighting again. But let’s not dwelve too much into it just yet. + highlighting again. But let’s not linger too much into it just yet. ## Spatial Sway -A few days after publishing my August Retrospective, I have learnt +A few days after publishing my August Retrospective, I have learned the existence of [Material Shell](https://material-shell.com), an extension for GNOME 3 that provides a very interesting user experience. @@ -39,13 +39,13 @@ horizontally (from one workspace to another), or horizontally, and you choose how many windows you want to see at once on your screen. And so for a few hours, I was a bit frustrated by the situation… -until I learnt about how one can actually manage and extend Sway +until I learned about how one can actually manage and extend Sway (the Wayland compositor I use for several years now) thanks to its IPC protocol. I spend like three days experimenting, first in Rust, then in OCaml[^ocaml], and by the end of the week, I had a first working prototype I called [Spatial Sway](https://github.com/lthms/spatial-shell). It works pretty -well, enough at least that I am using it daily for several weeks now. It feels -clunky at time, but it works well, and I have been able to write a +well; well enough that I am using it daily for several weeks now. It feels +clunky at times, but it works well, and I have been able to write a [Waybar](https://github.com/Alexays/Waybar) configuration heavily inspired on Material Shell UI. @@ -55,11 +55,11 @@ Material Shell UI. I have curated a setup that works pretty well, and I am familiar with the development tools. On the contrary, I had not written a line of Rust for at least a year, my Emacs configuration for this language was broken, and I - had lost all my fluancy in this language. Still, I was not expecting to + had lost all my fluency in this language. Still, I was not expecting to pick OCaml when I started this project. Overall, I am pretty satisfied with this turnout. Writing a hobbyist -software project is always nice, but the one you can integrate in +software project is always nice, but the ones you can integrate in your daily workflow are the best one. The last time I did that was [**keyrd**](https://sr.ht/~lthms/keyrd), my little keystrokes counting daemon[^keyrcount]. @@ -67,11 +67,11 @@ daemon[^keyrcount]. [^keyrcount]: 19,970,965 since I started using it at the time of writing this article -Anyway, lots remain to be said about Spatial Sway, but I might save +Anyway, lots remains to be said about Spatial Sway, but I might save it for a bit later. I still have some key features to implement -(notably, moving a window to another workspaces), then I will +(notably, moving a window to another workspace), then I will probably try to advertise it a bit. I am under the impression this -project could be of interest for other, and I would love to see it +project could be of interest for others, and I would love to see it used by folks willing to give a Material Shell-like experience a try, without having to deal with Gnome Shell. By the way, considering Sway is a drop-in replacement for i3, and that it @@ -93,24 +93,24 @@ I have been experimenting with `coqdoc`, to improve the readability of my Coq-related articles. Unfortunately, it looks like this tool is missing [a key feature I need](https://github.com/cpitclaudel/alectryon/issues/86). I might try to get -my hand dirty and implement it my self, if I find the time and the motivation +my hand dirty and implement it myself if I find the time and the motivation in the following weeks. Finally, reading about how [Xe Iaso’s talk about how she generates her -blog](https://xeiaso.net/talks/how-my-website-works) was very inspiring too me. -I can only suggest you to have a look. +blog](https://xeiaso.net/talks/how-my-website-works) was very inspiring to me. +I can only suggest that you have a look. -Though not to the same extend, Ialso think I have spent way too much effort in +Though not to the same extent, I also think I have spent way too much effort in my website. Most of my Coq-related articles are actual Coq program, expect the -articles about `coqffi` which are actual literate programs. Hell, this website -itself used to be a literate program of sort, until I stopped using my +articles about `coqffi` which are Org mode literate programs. Hell, this website +itself used to be a literate program of the sort, until I stopped using my homegrown literate programming toolchain **`cleopatra`** last month. At some point, I have even spent a bit of time to ensure most of the pages of this website were granted a 100/100 on websites like PageSpeed Insight[^goodnews]. I -had almost forgot. +had almost forgotten. [^goodnews]: Good news, I’ve just checked, and it still is! A lot remains to be done, but watching this talk made me reflect on -the job done. And opened my eyes to new perspective, too. We will +the job done. And opened my eyes to a new perspective, too. We will see what translates into reality. diff --git a/site/posts/StackedGit.md b/site/posts/StackedGit.md index 7e88721..3c0e45b 100644 --- a/site/posts/StackedGit.md +++ b/site/posts/StackedGit.md @@ -10,8 +10,8 @@ abstract: | # How I Use Stacked Git at `$WORK`{.bash} According to [my Lobste.rs history](https://lobste.rs/s/s6quvg/stacked_git), I -have run into [Stacked Git](https://stacked-git.github.io) in early April, -2021, and I remember its promises hit a soft spot. A few weeks later, I was +have run into [Stacked Git](https://stacked-git.github.io) in early April +2021, and I remember that its promises hit a soft spot. A few weeks later, I was submitting [a *pull request* to teach Stacked Git to sign commits](https://github.com/stacked-git/stgit/pull/100). It was all I needed to start using it at `$WORK`{.bash}, and now it has become a cornerstone of my @@ -25,9 +25,9 @@ present Stacked Git. The website introduces the tool as follows: > Stacked Git, *StGit* for short, is an application for managing Git > commits as a stack of patches. -There is a few things to unpack here. First and as its name suggests, Stacked +There are a few things to unpack here. First and as its name suggests, Stacked Git is a tool built on top of Git[^pijul]. It is *not* a brand new VCS, and as -a consequence you keep to use all your existing tools and plugins[^magit]. +a consequence you keep using all your existing tools and plugins[^magit]. Secondly, Stacked Git helps you curate your Git history, by turning your commits into patches, and your branches into stacks of patches. This speaks to me, maybe because I have been fascinated by email-based workflows for quite @@ -77,12 +77,12 @@ At a given time, a patch can either be (1) applied, (2) unapplied, or (3) hidden. On the one hand, if a patch is applied it is part of the Git history. On the other hand, unapplying a patch means removing it from the working branch (but not from the stack of patches of Stacked Git). If a patch becomes -unrelevant, but you don’t want to remove it entierely because it can become +irrelevant, but you don’t want to remove it entirely because it can become handy later, you can hide it. A hidden patch sits beside the stack of patches, and can be reintegrated if need be. -Analoguous to `git log` ---which allows you to visualize your Git history---, -`stg series` gives you a view the state of your stack of patches. Patches +Analogous to `git log` ---which allows you to visualize your Git history---, +`stg series` gives you a view of the state of your stack of patches. Patches prefixed with `+` (or `>`) are applied, while `-` means the patch is unapplied. Then, @@ -94,9 +94,9 @@ Then, - `stg goto NAME` unapplies or applies the necessary patches so that `NAME` becomes the top patch of the list of applied patches. -`HEAD` and the worktree are updated accordingly. +Both `HEAD` and the work tree are updated accordingly. -In addition, `stg sink` and `stg float` allow to reorganize your +In addition, `stg sink` and `stg float` allow reorganizing your stack of patches, moving patches around. Basically, they are like `git rebase -i`, but without having to use `$EDITOR`. @@ -105,7 +105,7 @@ Modifying patches is done with `stg refresh`. It’s akin to `git commit --amend`, except it is more powerful because you can modify any applied patches with the `-p` option. I’d always encourage you to `stg goto` first, because `stg refresh --p` remains unfortunately error prone (nothing prevents you to target +-p` remains unfortunately error-prone (nothing prevents you from targeting the wrong patch). But when used carefully, it can be very handy. @@ -114,17 +114,17 @@ It is akin to `git rebase --onto`, but more straightforward. What happens is Stacked Git pop all the patches of my stack, reset the `HEAD` of the current branch to `REF`, and tries applying the patches one by one In case of conflicts, the process stop, and I am left with an empty patch, and a dirty -worktree with conflicts to solve. The hidden gem is that, contrary to `git +work tree with conflicts to solve. The hidden gem is that, contrary to `git rebase`, the repository is not “in the middle of a rebase.” -Suppos there are many conflicting patches still waiting in my stack of patches, +Suppose there are many conflicting patches still waiting in my stack of patches, and an urgent task I need to take care of first. I can just leave them here. I can switch to another branch, and when I come back, I get my patches back. I call this feature “incremental rebases.” [^rebase]: Stacked Git is supposedly able to detect, during a rebase, which of your patches have been applied to your target branch. I’d rather use `stg - uncommit`{.bash} before do the rebase, though. + uncommit`{.bash} before doing the rebase, though. And that is basically it. In a nutshell, Stacked Git equips commits with the same features as branches. @@ -146,7 +146,7 @@ Stacked Git makes just everything so more convenient to me. I’ve been introduced to Git with a pretty simple workflow: I am supposed to start working on a feature, and once it’s ready, I -can commit, and move on to the next task on my todo list. +can commit, and move on to the next task on my to-do list. To me, this approach is backward. It makes you set your intent after the fact. @@ -154,7 +154,7 @@ With Stacked Git, I often try to plan my final history /before writing the very first line of code/. Using `stack new`, I create my patches, and take the time to write their description. -It helps me visualizing where I want to go. +It helps me visualize where I want to go. Then, I use `stack goto` to go back to the beginning of my stack, and start working. @@ -171,11 +171,11 @@ which I find very annoying, because it does not provide meaningful ways to compare two versions of your submission[^gitlab]. [^gitlab]: There is a notion of “versions” in Gitlab, but its ergonomics fall - short of my expectations for such tool. + short of my expectations for such a tool. -What we end up doing is creating “fixup commits”, and we push them +What we end up doing is creating “fixup commits,” and we push them to Gitlab so that reviewers can easily verify that their feedback -have correctly been taken into account. +has correctly been taken into account. A fixup commit is a commit that will eventually be squashed into another. @@ -227,7 +227,7 @@ For a few months, I have been involved in a project wherein we decided /not/ to fall in the same trap again. We agreed on a “planning of merge requests” and started working. The first merge request was soon opened. -We’ve nominated a “owner” to take care of the review, and the rest +We’ve nominated an “owner” to take care of the review, and the rest of the team carried on. Before the first merge request was merged, the second one was declared ready, and another owner was appointed. @@ -238,7 +238,7 @@ It turns out Stacked Git is a wonderful tool to help me keep this under control. I only have one branch, and I use the same workflow to deal with -feedbacks, even if they are coming from more than one one merge +feedback, even if they are coming from more than one merge request. To remember the structure of everything, I just prefix the name of my patches with a merge request nickname. @@ -253,9 +253,9 @@ So my stack will look something like this: ``` A reviewer leaves a hard-truth comment that requires a significant rework of -the oldest merge request? `stg goto` reverts my worktree in the appropriate +the oldest merge request? `stg goto` reverts my work tree in the appropriate state, and `stg push` allows me to deal with conflicts one patch at a time. If -at some point I need to spend more time on the oldest merge request, I can +I need to spend more time on the oldest merge request at some point, I can continue my work, knowing the patches related to the newest one are awaiting in my stack. diff --git a/site/posts/StackedGit2.md b/site/posts/StackedGit2.md index ac38e92..313901f 100644 --- a/site/posts/StackedGit2.md +++ b/site/posts/StackedGit2.md @@ -14,7 +14,7 @@ enough has changed to motivate a spin-off piece. ## Stacked Git is *Fast* -Firstly, it is important to state that my main complain about +Firstly, it is important to state that my main complaint about Stacked Git is now a thing of the past[^edit]! Stacked Git does not feel slow anymore, and far from it. This is because [Stacked Git 2.0 has been rewritten in Rust](https://github.com/stacked-git/stgit/discussions/185). While RiiR @@ -67,7 +67,7 @@ takes for a given MR to be integrated into the main branch. drawbacks too. During the past year, I’ve pushed fairly large commits which could have - been splitted into several smaller ones, for the sake of keeping my “one + been split into several smaller ones, for the sake of keeping my “one commit per MR” policy. I have also had to manage large stacks of MRs. My previous approach based on git branches did not scale well with @@ -122,7 +122,7 @@ these commits, and I need to publish each commit individually using The pragmatic answer is definitely to come back to git branches *for this particular use case*, but it's not the *fun* answer. So from -time to time, I try to experiment alternative approaches. My current +time to time, I try to experiment with alternative approaches. My current intuition is that, by adopting a naming convention for my patches, I could probably implement a thin tooling on top of Stacked Git to deal with dependents commits. diff --git a/site/posts/StronglySpecifiedFunctionsProgram.md b/site/posts/StronglySpecifiedFunctionsProgram.md index da07982..a16eca7 100644 --- a/site/posts/StronglySpecifiedFunctionsProgram.md +++ b/site/posts/StronglySpecifiedFunctionsProgram.md @@ -63,8 +63,8 @@ Proof. Defined. ``` -We have witness in my previous article about strongly-specified -functions that mixing proofs and regular terms may leads to +We have seen in my previous article about strongly specified +functions that mixing proofs and regular terms may lead to cumbersome code. From that perspective, `Program`{.coq} helps. Indeed, the `lock`{.coq} function @@ -85,7 +85,7 @@ Definition lock' (reg: SmramcRegister) Another way to "embed proofs in a program" is by specifying pre- and post-conditions for its component. In Coq, this is done using -sigma-types. +sigma types. On the one hand, a precondition is a proposition a function input has to satisfy in order for the function to be applied. For instance, a precondition @@ -108,8 +108,8 @@ Definition head {a} (l : list a | l <> []) ``` We recall that because `{ l: list a | l <> [] }`{.coq} is not the same as `list -a`{.coq}, in theory we cannot just compare `l`{.coq} with [x :: l'] (we need to -use `proj1_sig`{.coq}). One benefit on `Program`{.coq} is to deal with it using +a`{.coq}, in theory we cannot just compare `l`{.coq} with `x :: l'`{.coq} (we need to +use `proj1_sig`{.coq}). One advantage of `Program`{.coq} is to deal with it using an implicit coercion. Note that for the type inference to work as expected, the @@ -177,13 +177,13 @@ Arguments vnil {a}. ``` I had three functions in mind: `take`{.coq}, `drop`{.coq} and `extract`{.coq}. -I learned few lessons. My main take-away remains: do not use sigma-types, -`Program`{.coq} and dependent-types together. From my point of view, Coq is not +I learned a few lessons. My main takeaway remains: do not use sigma types, +`Program`{.coq} and dependent types together. From my point of view, Coq is not yet ready for this. Maybe it is possible to make those three work together, but I have to admit I did not find out how. As a consequence, my preconditions are defined as extra arguments. -To be able to specify the post conditions my three functions and +To be able to specify the post conditions of my three functions and some others, I first defined `nth`{.coq} to get the _nth_ element of a vector. @@ -258,7 +258,7 @@ Defined. As a side note, I wanted to define the post condition as follows: `{ v': vector A e | forall (i : nat | i < e), nth v' i = nth v i }`{.coq}. However, this made the goals and hypotheses become very hard -to read and to use. Sigma-types in sigma-types: not a good +to read and to use. Sigma types in sigma types: not a good idea. ```ocaml @@ -523,7 +523,7 @@ Qed. ## Is It Usable? This post mostly gives the "happy ends" for each function. I think I tried -to hard for what I got in return and therefore I am convinced `Program`{.coq} +too hard for what I got in return and therefore I am convinced `Program`{.coq} is not ready (at least for a dependent type, I cannot tell for the rest). For instance, I found at least one bug in Program logic (I still have to report it). Have a look at the following code: diff --git a/site/posts/StronglySpecifiedFunctionsRefine.md b/site/posts/StronglySpecifiedFunctionsRefine.md index 6f541c8..eb1fff9 100644 --- a/site/posts/StronglySpecifiedFunctionsRefine.md +++ b/site/posts/StronglySpecifiedFunctionsRefine.md @@ -18,19 +18,19 @@ yet hard to master. Fortunately, there are some very good readings if you want to learn (I recommend the Coq'Art). This article is not one of them. -In this article, we will see how to implement strongly-specified +In this article, we will see how to implement strongly specified list manipulation functions in Coq. Strong specifications are used to ensure some properties on functions' arguments and return value. It makes Coq type system very expressive. Thus, it is possible to specify in the type of the function `pop`{.coq} that the return -value is the list passed in argument in which the first element has been -removed for example. +value is the list passed as an argument in which the first element has been +removed, for example. ## Is This List Empty? It's the first question to deal with when manipulating lists. There are some functions that require their arguments not -to be empty. It's the case for the `pop`{.coq} function, for instance: +to be empty. It's the case for the `pop`{.coq} function, for instance it is not possible to remove the first element of a list that does not have any elements in the first place. @@ -41,7 +41,7 @@ two different worlds that do not mix easily. One solution is to write two definitions and to prove their equivalence. That is `forall args, predicate args <-> bool_function args = true`{.coq}. -Another solution is to use the `sumbool`{.coq} type as middleman. The +Another solution is to use the `sumbool`{.coq} type as middlemen. The scheme is the following: - Defining `predicate : args → Prop`{.coq} @@ -53,7 +53,7 @@ Definition predicate_b (args) := if predicate_dec args then true else false. ``` -### Defining the `empty`{.coq} Predicate *) +### Defining the `empty`{.coq} Predicate A list is empty if it is `[]`{.coq} (`nil`{.coq}). It's as simple as that! @@ -134,7 +134,7 @@ article. ## Defining Some Utility Functions -### Defining `pop`{.coq} *) +### Defining `pop`{.coq} There are several ways to write a function that removes the first element of a list. One is to return `nil` if the given list was @@ -179,7 +179,7 @@ From the following goal: list a ``` -Using the `refine`{.coq} tactic naively, for instance this way: +Using the `refine`{.coq} tactic naively, for instance, this way: ```coq refine (match l with @@ -203,14 +203,14 @@ our incomplete Gallina term, found a hole, done some type-checking, found that the type of the missing piece of our implementation is `list a`{.coq} and therefore has generated a new goal of this type. What `refine`{.coq} has not done, however, is -remember that we are in the case where `l = []`{.coq}. +remembering that we are in the case where `l = []`{.coq}. We need to generate a goal from a hole wherein this information is -available. It is possible using a long form of `match`{.coq}. The +available. It is possible to use a long form of `match`{.coq}. The general approach is this: rather than returning a value of type -`list a`{.coq}, our match will return a function of type [l = ?l' -> -list a], where `?l`{.coq} is value of `l`{.coq} for a given case (that is, -either `x :: rst`{.coq} or `[]`{.coq}). Of course, As a consequence, the type +`list a`{.coq}, our match will return a function of type `l = ?l' -> +list a`{.coq}, where `?l`{.coq} is a value of `l`{.coq} for a given case (that is, +either `x :: rst`{.coq} or `[]`{.coq}). Of course and as a consequence, the type of the `match`{.coq} in now a function which awaits a proof to return the expected result. Fortunately, this proof is trivial: it is `eq_refl`{.coq}. @@ -245,20 +245,20 @@ Defined. ``` It's better and yet it can still be improved. Indeed, according to its type, -`pop`{.coq} returns “some list”. As a matter of fact, `pop`{.coq} returns “the -same list without its first argument”. It is possible to write -such precise definition thanks to sigma-types, defined as: +`pop`{.coq} returns “some list.” As a matter of fact, `pop`{.coq} returns “the +same list without its first argument.” It is possible to write +such precise definition thanks to sigma types, defined as: ```coq Inductive sig (A : Type) (P : A -> Prop) : Type := exist : forall (x : A), P x -> sig P. ``` -Rather that `sig A p`{.coq}, sigma-types can be written using the +Rather than `sig A p`{.coq}, sigma-types can be written using the notation `{ a | P }`{.coq}. They express subsets, and can be used to constraint arguments and results of functions. -We finally propose a strongly-specified definition of `pop`{.coq}. +We finally propose a strongly specified definition of `pop`{.coq}. ```coq Definition pop {a} (l : list a | ~ empty l) @@ -328,11 +328,11 @@ let pop = function ``` If one tries to call `pop nil`{.coq}, the `assert`{.coq} ensures the call fails. Extra -information given by the sigma-type have been stripped away. It can be +information given by the sigma type has been stripped away. It can be confusing, and in practice it means that, we you rely on the extraction mechanism to provide a certified OCaml module, you _cannot expose -strongly-specified functions in its public interface_ because nothing in the -OCaml type system will prevent a miseuse which will in practice leads to an +strongly specified functions in its public interface_ because nothing in the +OCaml type system will prevent a misuse which will in practice leads to an `assert false`{.ocaml}. *) ## Defining `push`{.coq} @@ -357,7 +357,7 @@ let push l a = ## Defining `head`{.coq} Same as `pop`{.coq} and `push`{.coq}, it is possible to add extra information in the -type of `head`{.coq}, namely the returned value of `head`{.coq} is indeed the firt value +type of `head`{.coq}, namely the returned value of `head`{.coq} is indeed the first value of `l`{.coq}. ```coq @@ -376,7 +376,7 @@ It's not a surprise its definition is very close to `pop`{.coq}. end eq_refl). ``` -The proof are also very similar, and are left to read as an exercise for +The proof is also very similar, and are left to read as an exercise for passionate readers. ```coq @@ -399,7 +399,7 @@ let head = function ## Conclusion -Writing strongly-specified functions allows for reasoning about the result +Writing strongly specified functions allows for reasoning about the result correctness while computing it. This can help in practice. However, writing these functions with the `refine`{.coq} tactic does not enable a very idiomatic Coq code. |