Blogposts in Thomas Letan's Website
What happened in February 2026? meta vibecoding Time flies. February was a productive month, and I got many things done—with the help of my coding assistant , that is. I haven’t joined the “I haven’t written a single line of code for quite some time” flock just yet, but I am close. At the same time, I feel like I’m still locked in beginner mode. Like I have still to really tap into what agentic…
Teaching Firefox About slack:// URLs releases I’ve been using Slack at $WORK for the past 5 (!) years. I don't know why, but it looks like Firefox does not know what to do with the slack:// URLs out of the box Try logging in Slack when your browser does not let Slack know authentication concluded successfully. The worst thing? Sometimes it works, sometimes it doesn’t. . It could be an issue on my…
What Happened in January 2026? meta vibecoding This is my first retrospective in quite a while—I have yet to make writing these logs a real habit of mine. That being the case, so much happened this month that this article felt like the obvious thing to do. tinkerbell ’s First Month On January 5th, I published my account of migrating my website to a completely new setup . Not only am I very proud…
How I Want to Use LLMs in 2026 opinions vibecoding I would like to thank Xavier Van de Woestyne for his feedback and careful review. Agentic tools are here, and they are here to stay. I don’t think it is an overstatement to say that LLMs are completely reshaping our day-to-day life. Even if mass adoption has yet to happen We are seeing more and more public statements from key figures of our…
I Cannot SSH Into My Server Anymore (And That’s Fine) coreos docker meta self-hosting terraform vultr I would like to thank Yann Régis-Gianas, Sylvain Ribstein and Paul Laforgue for their feedback and careful review. To kick off 2026, I had clear objectives in mind: decommissioning moana , my trusty $100+/month VPS, and setting up tinkerbell , its far less costly successor. On the one hand, I have…
Peer-Programming in Modern OCaml with ChatGPT and Gemini ocaml vibecoding It is June 2025, and LLMs are everywhere and do everything now. I have never been a diligent adopter of them myself. The past few months, I started to feel a bit “left out,” though. Colleagues and friends are starting to integrate LLM-powered tools into their personal toolkit, with notable successes. Early May, I decided to…
What Happened in 2024? meta We are done with 2024, and now is a good time to reflect on what has happened over the past 12 months. I was not planning to, but my feed convinced me to give it a try . Plus, it is a good opportunity to revive my “ Retrospective ” series. Free and Open Source Software I’ve been a “prolific contributor” at $WORK , but less so with my personal projects. Spatial Shell…
Serving This Article from RAM for Fun and No Real Benefit docker meta ocaml In 2022, Xe Iaso published a transcript of their talk on how their website was working at the time . In a nutshell, their approach consisted of a server preprocessing the website from its source at startup, then serving its contents from memory. If you have not already, I can only encourage you to read the article or watch…
On Vestigial Structures satire ocaml Do you know what vestigial structures are? This write-up is a slightly modified version of a commit description I have written for $WORK with some help from ChatGPT . In a nutshell, they are remnants of structures that were functional in an ancestral species but have lost much or all of their original function in the descendant species. For instance, some…
Introducing bepo-tsrn.nvim neovim releases It is not much, but I have recently published on GitHub what can be considered my very first Neovim “plugin.” bepo-tsrn.nvim is a zero-configuration, global plugin for Neovim which remaps default Neovim bindings for the Bépo keyboard layout. It started as a fork of bepo.nvim with two significant changes: hjkl are remapped to tsrn instead of ctsr . hjkl as…
Installing a LUKS-Encrypted Arch Linux on a Vultr VPS self-hosting vultr I’ve been a happy customer of Vultr for three years now. For one, this little corner of the Internet is hosted on one of their VPS, along with other services I have self-hosted. Recently, I have decided to migrate to a new VPS with more disk space and more powerful vCPUs. In this article, I describe how I have set up the host…
Using git maintenance with Encrypted SSH Keys workflow git This year, I went to FOSDEM 2024 . It was nice and cosy crowded, and I really enjoyed my time there. The very last talk I could attend to before having to leave for the train station was “ So You Think You Know Git ” by Scott Chacon . If you haven’t already, go and watch it. It is a very good and educational presentation. You will learn…
Building Static Binaries for OCaml Projects ocaml Building static binaries can come in handy. Most notably, when the time comes to distribute executables. I should know, because I spend a bit of time recently preparing for the 6th release of Spatial Shell , and part of that time was ensuring that folks on Linux unwilling to build an OCaml project from source could still give my project a shot.…
Spatial Shell 6th Release Might Be the Charm spatial-shell releases After a first call for testers that could have been more effective if only the building instructions listed in the README were correct , I am quite happy to announce the 6th release for Spatial Shell that, I believe, is pretty usable for someone who isn’t me . What’s Spatial Shell Already? In a nutshell, Spatial Shell implements a…
The Free and Open Source Software Projects This Website is Built Upon in June 2023 meta In the past, I had a page called “Thanks!” dedicated to listing the free and open source software projects I was relying on to create this website. Sadly, this page was dropped during my latest overhaul, which is a shame because I do think it is important to acknowledge these fantastic projects without which…
Extensible Records in OCaml Using dmap ocaml dmap is a library to create and manipulate heterogeneous maps. It features a very straightforward API which leverages the common trick of tagging the type of the keys with a parameter specifying the types of the associated values This article assumes readers are familiar with GADTs. . That is, given 'a key the type of keys of a heterogeneous map t ,…
The Chaotic Debut of My Software Projects opinions I am no stranger to the exciting feeling of starting new projects. By dint of repeating this “exercise” over the years, I have come to build an intuitive process which works for me. In this write-up, I want to give a try at describing it, both for future references and in the hope that this might start interesting conversations. I am curious to…
What happened since December 2022? emacs meta neovim releases spatial-shell Initially, I started this “What happened” series as an exercise to publish more regularly on this website. Suffice to say, I haven’t done a particularly impressive job in that regard, which only means I have a lot of room for improvement. Anyway, if the first few months of 2023 has been mostly $WORK focus, the same cannot…
Neovim, OCaml Interfaces, Tree-Sitter and LSP ocaml neovim Can we all agree that witnessing syntax highlighting being absolutely off is probably the most annoying thing that can happen to anybody? I mean, just look at this horror. Syntax highlighting being absolutely wrong. What you are looking at is the result of trying to enable tree-sitter for OCaml hacking and calling it a day. In a nutshell,…
Spatial Shell: Call For Testers spatial-shell In August 2022, I have discovered Material Shell . A few weeks later, I had pieced together a working prototype of a dynamic tiling management “a la Material Shell” for sway . By October, the project was basically fulfilling my needs, and I had already started to use it on my workstation I tried so you do not have to: having my graphical session going…
Patch Dependencies for Stacked Git git opinions Every time I catch myself thinking about dependencies between changeset of a software project, the fascinating field of patch theories comes to my mind. A “patch theory” usually refers to the mathematical foundation behind the data model of so-called Patch-based DVCS like Darcs and Pijul. More precisely, a patch theory is an encoding of the state of…
How I Keep Using Stacked Git at $WORK git workflow One year ago, I have published an article summarizing my experience using Stacked Git at $WORK . Twelve months later, enough has changed to motivate a spin-off piece. Stacked Git is Fast Firstly, it is important to state that my main complaint about Stacked Git is now a thing of the past For fairness, I have removed the related section in my…
What happened in October and November 2022? spatial-shell nanowrimo coqffi It is November 19 today, and I’m one month and 4 days late for the October Retrospective! Truth is, $WORK has been intense lately, to a point where I have not made much progress on my side projects. Anyway. I have implemented the last feature I was really missing in my daily use of Spatial Sway: moving windows to adjacent…
What happened in September 2022? spatial-shell meta It is September 18 today, and it has already been a month since I decided to start these retrospectives. This means it is time to take a step back and reflect of what happened these past few thirty days or so There is the shocking news that I have started to use syntax highlighting again. But let’s not linger too much into it just yet. . Spatial…
What happened in August 2022? emacs meta Without further ado, let’s take a look at what was achieved for the last thirty days or so. Emacs I have started tweaking and improving my Emacs configuration again After having used Emacs for seven years now, I am nowhere close to consider my configuration as a done project. I really envy developers who are using their editor with little to no…
Writing a Function Whose Argument is a Polymorphic Function in OCaml ocaml In OCaml, it is not possible to write a function whose argument is a polymorphic function. Trying to write such a function results in the type-checker complaining back at you. let foo ( type a b) id (x : a) (y : b) = (id x, id y) Line 1, characters 50-51: 1 | let foo (type a b) id (x : a) (y : b) = (id x, id y);; ^ Error:…
How I Use Stacked Git at $WORK git workflow According to my Lobste.rs history , I have run into Stacked Git 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 . It was all I needed to start using it at $WORK , and now it has become a cornerstone of my development workflow. What is Stacked…
Implementing an Echo Server in Coq with coqffi.1.0.0 coq ocaml coqffi In this article, we will demonstrate how coqffi can be used to implement an echo server, i.e. , a TCP server which sends back any input it receives from its clients. In addition to coqffi , you will need to install coq-simple-io . The latter is available in the released repository of the Opam Coq Archive . opam install…
coqffi.1.0.0 In A Nutshell coq ocaml coqffi For each entry of a cmi file (a compiled mli file), coqffi tries to generate an equivalent (from the extraction mechanism perspective) Coq definition. In this article, we walk through how coqffi works. Note that we do not dive into the vernacular commands coqffi generates. They are of no concern for users of coqffi . Getting Started Requirements The…
Pattern Matching on Types and Contexts coq In the a previous article 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 will refine the current goal by using an inductive principle dedicated to the…
Ltac is an Imperative Metaprogramming Language coq Coq is often depicted as an interactive proof assistant, thanks to its proof environment. Inside the proof environment, Coq presents the user a goal, and said user solves said goal by means of tactics which describes a logical reasoning. For instance, to reason by induction, one can use the induction tactic, while a simple case analysis can rely…
Mixing Ltac and Gallina for Fun and Profit coq 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…
Proving Algebraic Datatypes are “Algebraic” coq Several programming languages allow programmers to define (potentially recursive) custom types, by composing together existing ones. For instance, in OCaml, one can define lists as follows: type 'a list = | Cons of 'a * 'a list | Nil This translates in Haskell as data List a = Cons a ( List a) | Nil In Rust as enum List <A> { Cons (A, Box <List<a>>),…
A Study of Clight and its Semantics coq CompCert is a certified C compiler which comes with a proof of semantics preservation. What this means is the following: the semantics of the C code you write is preserved by CompCert compilation passes up to the generated machine code. I had been interested in CompCert for quite some times, and ultimately challenged myself to study Clight and its semantics.…
Release of colorless-themes-0.2 releases I have tagged and released a new version of colorless-themes . The motivation behind modifying the version number is an important breaking change regarding how the colorless-themes-make macro shall be used. Before 0.2 , the macro was calling deftheme and provide-theme itself. In practices, it meant the actual themes were not using these two functions…
A Literate Toolchain To Build This Website meta literate-programming emacs Important What you are reading is actually the rendered version of a Markdown document that was manually “translated” from the Org original document, named Bootstrap.org . Bootstrap.org was probably complete gibberish for anyone who isn’t me. This version was actually heavily reworked to try to fix that. In any case, the…
I am no longer a PhD. student research It has been a long journey —4 years, 10 days— but I have completed my PhD on October 25, 2018. The exact title of my PhD thesis is “ Specifying and Verifying Hardware-based Security Enforcement Mechanisms ”. Abstract In this thesis, we consider a class of security enforcement mechanisms we called Hardware-based Security Enforcement (HSE). In such mechanisms,…
Discovering Common Lisp with trivial-gamekit lisp I always wanted to learn some Lisp dialect. In the meantime, lykan —my Slayers Online clone— begins to take shape. So, of course, my brain got an idea: why not writing a client for lykan in some Lisp dialect? Spoiler alert: this wasn’t the most efficient approach for the lykan project. But it was fun. I asked on Mastodon if there were good game…
Extensible Type-Safe Error Handling in Haskell haskell A colleague of mine introduced me to the benefits of error-chain , a crate which aims to implement “ consistent error handling ” for Rust. I found the overall design pretty convincing, and in his use case, the crate really makes error handling clearer and flexible. I knew Pijul was also using error-chain at that time, but I never had the…
Monad Transformers are a Great Abstraction haskell Caution Time has passed since the publication of this article. Whether or not I agree with its conclusions is an open question. Monad Transformers are a great abstraction, but nowadays I would most certainly choose another approach. Monads are hard to get right. I think it took me around a year of Haskelling to feel like I understood them. The…
Rewriting in Coq coq I have to confess something. In the codebase of SpecCert lies a shameful 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…
Implementing Strongly-Specified Functions with the Program Framework coq The Theory If I had to explain Program , I would say Program is the heir of the refine tactic. It gives you a convenient way to embed proofs within functional programs that are supposed to fade away during code extraction. But what do I mean when I say "embed proofs" within functional programs? I found two ways to do it.…
Implementing Strongly-Specified Functions with the refine Tactic coq I started to play with Coq, the interactive theorem prover developed by Inria, a few weeks ago. It is a very powerful tool, 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…