Over the past years, I have tried to capitalize on my findings. What I have lacked in regularity I made up for in subject exoticism.
If you like what you read, have a question or for any other reasons really, you can shoot an email, or start a discussion on whichever site you like (I personnaly enjoy Lobste.rs very much).
About Coq
Coq is a formal proof management system which provides a pure functional language with nice dependent types together with an environment for writing machinechecked proofs.
 Proving Algebraic Datatypes are “Algebraic”

The set of types which can be defined in a language together with
+
and*
form an “algebraic structure” in the mathematical sense, hence the name. It means the definitions of+
and*
have to satisfy properties such as commutativity or the existence of neutral elements.  A Study of Clight and its Semantics
 Clight is a “simplified” C AST used by CompCert, the certified C compiler. In this writeup, we prove a straighforward functional property of a small C function, as an exercise to discover the Clight semantics.
 Implementing and Certifying a Web Server in Coq
 An explanation on how to write an almost pure Coq, and working (albeit minimal) HTTP server.
 Ltac 101
 Ltac is the “tactic language” of Coq. It allows for writing proof scripts which construct proof terms later checked by Coq.
 Rewriting in Coq

The
rewrite
tactics are really useful, since they are not limited to the Coq builtin equality relation.  A Series on StronglySpecified Funcions in Coq

Coq
Prop
sort allows for defining properties function arguments have to satisfy, such that using such a function requires providing a proof the property is satisfied.
About Haskell
Haskell is a pure, lazy, functional programming language with a very expressive type system.
 Extensible, TypeSafe Error Handling In Haskell
 Ever heard of “extensible effects?” By applying the same principle, but for error handling, the result is nice, typesafe API for Haskell, with a lot of GHC magic under the hood.
 Monad Transformers are a Great Abstraction
 Monads are hard to get right, monad transformers are harder. Yet, they remain a very powerful abstraction.
About Common Lisp
Common Lisp is a venerable programming languages like no other I know.

Discovering Common Lisp with
trivialgamekit
 From the creation of a Lisp package up to the creation of a standalone executable.
About this website
One of my goal with this website is for it to feel simple, but the truth is under the hood it is generated from a bunch of files using a notthatsimple process.
 A Series on Generating this Static Website

This series consolidates the
cleopatra
generation processes used to build this website. That is, each writeup is a literate program responsible for a particular step of the build process, and you are guaranteed that the code you read is the code that has been used to generate the HTML page you read it from.  Thanks!
 If it were not for many awesome FOSS projects, this corner of the Internet would not exist. This is my attempt to give welldeserved credit to them and their creators.

cleopatra
the First 
This writeup is the literate program of the first version of
cleopatra
, before it became a commandline program implemented in Rust.