The article is written in Coq
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
Require Import Coq.Lists.List.
Require Import Io.All.
Require Import Io.System.All.
Require Import ListString.All.

Import ListNotations.
Import C.Notations.

Definition hello_world (argv : list LString.t) : C.t System.effects unit :=
  System.log (LString.s "Hello world!").