joomy's blog

A write-up on why I don't give in to the hype and switch to Lean for formal verification of programs.

A short essay about why I refuse to learn complex language features like type-level programming in Haskell and first-class modules in OCaml.

Tracing the origin of the terms "intrinsic" and "extrinsic" in formal verification and programming languages.

I spent a week at the main functional programming conference and got to talk to my heroes, so here are some reflections.

Omitting the diacritics is a common phenomenon in languages such as Turkish and Serbo-Croatian.

The Idris community is not so fond of implicit conversions, I think they're a useful and powerful tool that are easy to misuse.

GHC.Proof is a great hack and I wanted to add another hack on top of it.

I will be giving lectures on Functional Programming in Haskell next semester.

My reflection on how I felt when I was adapting to an English-speaking environment.

I built a pseudo-Prolog that tries to answer queries by building the least Herbrand model, as a final project for a class.