Programming Languages Journal


I have come to a point in my Haskell journey where I should start learning about other programming languages (PL) fields. Towards the end of my FP journal, I started diving into Category Theory and formal verifications, endeavours that shouldn’t be documented in a “FP Journal”. As such, I’ve decided to start a PL journal, documenting all of my PL ventures. Unlike the previous journal, I do not plan to elaborate on the concepts I made sense of, as these elaborations often turn into word rambles in the moment.



Understanding the relationships between LTL (Linear Temporal Logic), Haskell, model-checkers, and proof assistants. Conclusion: TLA+ (model checker) can be used to model LTL statements and verify them. There exists LTL libraries in Haskell but they appear to be more data modelling purposes.


  • Chris (from work) sent me two papers:
  • Watched a video on linear logic. Everyday I’m hearing 5 new jargons, at the end of this week I ought to layout a taxonomy of the topics.


1st to 14th

  • Read the first 10 pages of the Lamport’s TLA paper that covers TLA motivation and semantics.
  • Watched the first lecture of RWTH Aachen University’s Model Checking course.
  • Talked to ChatGPT a lot to derive a taxonomy of formal verifications technique. Lectures do better jobs covering these types of information though — ChatGPT don’t really come up with memorable sayings.
  • Came across Linear Types, didn’t understand much.
  • Submitted my first paper ever (it’s on program analysis) to SCAM’23! I can reveal more if it gets accepted.
  • Read the intro of Pierce’s Software Foundations.
  • Read the first two chapter of Pierce’s TAPL — currently, I don’t find type theory as interesting as formal verifications. Though, I do believe that enjoyment is a linear combinations of the interestingness of the topic’s pure abstractions, the topic’s applicability, and one’s current understanding of the field. When it comes to type theory, I don’t have any of these.

15th to 19th

  • Read the docs of the servant library thoroughly: It’s the first library I encountered that uses DataKinds.
  • Read up on the expression problem (encountered through servant’s paper). Supposedly, Object Algebras of OOP or advanced Haskell type features can address it.
  • Going back to reading Milewski’s Category Theory for Programmers because I should be knowing what Kelsili Arrow and natural transformations are at this point.
    • Finished Chapter 3. Interesting idea: Think of functions in their uncurried form more. If I think of mappend as m -> (m -> m), I can see it as a mapping between an element of a monoid set to a function acting on that set!

Week 4

  • Listened to two episodes of the Haskell Interlude podcast: One with Gabriella Gonzalez, and one with Graham Hutton. Professor Hutton’s honesty and passion was, simply put, inspiring. The also-inspiring Gabriella mentioned two interesting things I’ll look into: Monad Reader and Dhall.
  • Listened to Conal Elliot talking about the lost elegance of computation. Unique and poignant philosophy, inspired by Conal’s passion, I ought to read John Backus’s famou 1977 Turing award lecture and read into FRP.
  • Read Monad Reader issue 19; learned about the Coroutine monad; I was able to use Iteratee and Generator to successfully implement a basic sketch of a program for work.


Week 1

  • Spent a weekend in FRP via Heinrich’s guide. Big idea: Behaviors are continous and Events are discrete, but, they can be easily composed and transformed to one another.
  • React-banana uses MonadMoment, which is also a MonadFix. I tried reading MonadFix is Time Travel. I only partially understood what’s going on even with after reading another article because I lack a complete understanding of laziness, thunks, and seq, so, I started reading Haskell wikibook’s laziness article.

Week 2

  • Finished my internship at TwoSix technologies, looking forward in returning as a formal methods researcher next summer!
  • Coming across the following for the first time: Refinement types, cubic type theory, the K framework.
  • I want to dedicate my time fully to reading 2 materials: Software Foundations (SF) and the Milewski’s Category Theory handbook, until school begins.
  • Finished the Basics chapter of SF’s Logical Foundations (LF) book. Good old functional programming!
  • Read Chapter 5-8 of the category theory book. I need to spend some time to gather more examples…