iiinova — where your digital self keeps evolving

Tiago Cogumbreiro @forkjoin.bsky.social · 27/09/2026

I have been having fun remembering I enjoy pixel art, by designing an android app icon. TIL, because of zoom+high res less detail makes icon more discernable.

020

Tiago Cogumbreiro @forkjoin.bsky.social · 24/09/2026

Even DeepSeek 4.1 is amazing at building GNOME apps, screenshot below as example, cost me 40 cents. Claude helped me cross compile an OCaml tool into JS, a C++ tool into wasm, linking to Z3 from npm, and then all 3 talk to each other via JS FFI, so I assume generating GNOME bindings would be easy.

210

Tiago Cogumbreiro @forkjoin.bsky.social · 31/03/2026

I'm getting closer to having an e-graphs library that can be shared with others. I'm porting some of the tutorials from Egg to finetune the UX and to see if I can reproduce some of the functionality. I am really enjoying ODoc+Dune! Nice combo.

A screenshot of Egg's Getting Started guide ported to an OCaml API.

000

Tiago Cogumbreiro @forkjoin.bsky.social · 15/01/2026

I think my macos build of faial seems to be working again. I would be very appreciated if you have an Apple laptop (m1 or newer) and you can the give binary dist of faial a go, you'll be able to find the link on top of the readme: gitlab.com/umb-svl/faial

Screenshot of git history showing 14 commits.

010

Tiago Cogumbreiro @forkjoin.bsky.social · 25/10/2025

The tool is all implemented in OCaml. The monadic-design pattern of parsing JSON comes from what I learned in Faial <https://gitlab.com/umb-svl/faial/> and I think it looks neat.

A screenshot of OCaml code showing some JSON deserialization code.

010

Tiago Cogumbreiro @forkjoin.bsky.social · 25/10/2025

The output is Markdown-formatted and the tool can figure out your Rocq project. I've been using this to help Claude Code help me, with some success. I have some scratch files in the project, including playing around with Fleche, but I haven't figured that code base yet.

A screenshot of `proof-ls` in action, showing a proof state.

100

Tiago Cogumbreiro @forkjoin.bsky.social · 19/06/2025

I'm learning to use Claude code for my Rocq proof development. First rule of fight club: If ANY proof attempt fails to compile, STOP IMMEDIATELY. Otherwise, Claude just exhausts my tokens.

**CRITICAL RULE**: If ANY proof attempt fails to compile, STOP IMMEDIATELY.

000

Tiago Cogumbreiro @forkjoin.bsky.social · 25/05/2025

Original post: types.pl/@liamoc/1145...

010

Tiago Cogumbreiro @forkjoin.bsky.social · 12/05/2025

Here's a short demo I gave to my students on proving a simple result without ltac (functional style). #Rocq gist.github.com/cogumbreiro/...

`nat_ind (fun x => x + 0 = x) eq_refl (fun n IH => eq_S (n + 0) n IH)`

110

Tiago Cogumbreiro @forkjoin.bsky.social · 28/02/2025

I bought @unpackinggame.com. The objective is to organize a room that you just moved in. You're unpacking these boxes and placing the items in drawers, closets etc. I love the irony of playing Unpacking while being at a messy room that I should be cleaning. It's a unique game in that way.

000

Tiago Cogumbreiro @forkjoin.bsky.social · 29/12/2024

I got it to work! I had to prove equality "axiomatically", but it worked out. gist.github.com/cogumbreiro/...

000

Tiago Cogumbreiro @forkjoin.bsky.social · 29/12/2024

I tried this, but not getting much farther. That being said, this is my first time playing with GADTs, so I'm just mashing keys.

100

Tiago Cogumbreiro @forkjoin.bsky.social · 07/12/2024

3 of my favorite home-brewed tactics are - invc H (which does `inversion H; subst; clear H`) - `rename_hyp PATT as H`, which renames an assumption given a pattern PATT with name H - `invc_hyp PATT`, which performs `invc` on an assumption given by a pattern PATT. #RocqLang #CoqLang

Small excerpt in Rocq showing the 3 tactics in action.

110

Tiago Cogumbreiro @forkjoin.bsky.social · 01/12/2024

Early steps on verifying time for imperative programs.

Source: Nielson's "A Hoare-like proof system for analysing the computation time of programs," 1987.

Source: "Semantics with Applications: An Appetizer" by Nielson and Nielson, 1992.

000

Tiago Cogumbreiro @forkjoin.bsky.social · 26/11/2024

Oh, I just tried the reverse exercise and it also did pretty well! The future is now. I'm loving the idea of generating latex from this.

A few inference rules generated from the OCaml code.

A snippet of a static analysis algorithm written in OCaml.

010