# Programming Languages Journal

### Foreword

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.

## June

**28th**

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.

**29th**

- Chris (from work) sent me two papers:
- Runtime Verification for LTL and TLTL
- Alternating Automata and Program Verification These papers supposedly describe how LTL statements can really be translated (down?) to a FSM (Finite State Machine). From there, any language can be used to implement this FSM (since a simple FSM is just a
`while`

loop +`switch`

statements). I will zoom in on these tomorrow.

- 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.

## July

**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!

- Finished Chapter 3. Interesting idea: Think of functions in their uncurried form more. If I think of

**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.

## August

**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…