Independent Nix/Haskell contractor, formal methods and NixOS infrastructure

I'm an independent contractor working on Nix, NixOS, and Haskell infrastructure. My focus is production systems where correctness and reproducibility matter more than velocity alone.

I maintain nix-effects, which embeds algebraic effects and a dependent type checker in pure Nix. The engineering novelty is running this in a language with no native support for algebraic data types, pattern matching, or recursive let-bindings as usually understood. I run the Nix and Colmena deployment stack for Lie-Størmer-senteret, Norway's national centre for mathematics.

My background is category theory. MSc from Oxford. Co-author with Paolo Perrone on "Categorical algebra of conditional probability" (arXiv 2502.14941), presented at SYCO 13 in London. I read Lean, Agda, and Isabelle at working level.

Based in Tromsø, Norway. Fully remote across Europe. Registered as Mika Bohinen ENK.