Ooqui inspired me to start a series on Colour actually. As a dev you'll naturally know a thing or two about colour or perception but this guy goes deep and it's super fascinating content I agree. Super unique too, I had never heard about most of the stuff he researches before watching his videos.
I'm working on a series about milk at the moment but I'll get back to colours eventually, there's a lot more to tell there :) Will make sure to give color spaces and gamut special treatment!
I specifically resonated with your post [Please just give me a programming language man](https://t3.at/blog/2025-08-07-configuramming/).
In my case the frustration came from having to figure out the github actions yml. And I am thankful to have not bothered going doing the ansible rabbit hole!
I hope you get time to work on making it mobile friendly, since it can be a time consuming endeavor and would encourage you to have an RSS feed for your blog!
> Now.. we’re really reaching the boundaries of my knowledge here, but as I understand, not all theorems in mathematics are provable by constructive proofs, which is what the Curry-Howard isomorphism gives us access to. So there will always be mathematical truths that are outside the reach of any type system, that are provable under for example the set of axioms known as Zermelo-Fraenkel set theory with the axiom of choice (ZFC). ZFC is provably more expressive than λC or any other type system we can come up with, because the axiom of choice gives us access to non-constructive proofs.
I am no expert on type theory nor logic but I think there are a few errors here:
- Curry-Howard is not restricted to intuitionistic logic / constructive type theories.
- Type systems can be made arbitrarily expressive.
- Non-constructive proofs exist in pure ZFC, too. They don't depend on assuming the Axiom of Choice. The core ingredient is the Law of Excluded Middle / proofs by contradiction.