Worst summer of my life.

"Can you even measure the resistance with a multimeter?" says a person with ChatGPT on hand while trying to teach me to do the thing I've done for 3.5 years in the past.

Is there something wrong with people or else what is the cause of this kind of behavior?

Freiheit

It's been a year since I achieved career freedom. I was truly happy back then, and I'm even happier now.

To be more precise, this has meant working with a good salary, fully remote, AND with a flexible schedule. A magnificent combination. I'm so thankful for my friends who have cherished and supported me and my passions. I'm especially thankful for the Russian Haskell community and the other chats I'm in. I've had my fair share of people there to look up to and they, thankfully, still haven't disappointed. (It's a topic that has led me to some interesting conclusions. See: Vorbild)

I've had a significant boost within this period. I got my hands on type theory, proof assistants, formal specification languages, and more. I also successfully used Alloy 6 in production. Even if I only formalized a small part of our app, it was something. Then I got a Haskell job (more on this in the near future).

However, I've learned it's not a perfect situation. The downside of working fully remote with a flexible schedule is that your family might not take your job seriously. So, if you live with them, try to get to an office at least once or twice a week. Better yet: live alone, explore the world (digital nomad visas are great for this), and embrace solitude.

Looking forward to achieving even greater freedom.

Unterschied

Lean now has a Computer Science library: cslib.

I'm pretty excited about this, especially since it includes a lambda calculus implementation. I've spent a good amount of time on that topic myself and even had aspirations of somehow contributing my own implementation to the ecosystem.

Comparing our implementations, they're almost the same. This isn't surprising of course, considering that an untyped lambda calculus is a well-trodden path and correct implementations will naturally converge.

What really caught my eye, though, was the difference in style for capture-avoiding substitution. You can see my (substGensym) and Fabrizio Montesi's (subst) implementations side-by-side.

The difference shows a real contrast in thinking. His approach is beautiful: he uses the HasFresh typeclass to push the responsibility for generating fresh variables onto the type system and the call site. This keeps the signature clean.

I, a bachelorless pseud, went with a State monad. While it works, it introduces complexity that makes proving things a nightmare down the line. Things get so complex that you will shit your pants and kill your roommate. I even abandoned some proofs because of how crazy it got. His implementation is better by a large margin.

Still, I'm happy with my own code. The book I was using didn't fully define capture-avoiding substitution, so I had to experiment and ended up independently rediscovering the same solution. It’s a great feeling. Proof assistants are amazing for this kind of instant feedback, and it's cool to look back at your old code and see how far you've come.

There are two wolves inside me

One solves problems with prop drilling

One solves them by cluttering the return type

Both define substitution wrong

Both of those implementations had a bug that broke the scoping.

Explanation in this thread: nitter, twitter.

Thankfully, effectfully masterfully caught it, and now both of them are fixed and work beautifully:

- keilambda/ttfpi
- leanprover/cslib

I fucking love recursion-schemes.

First iteration of the DPLL-based SAT solver is ready: SAT.hs

There's a room for improvement of course. So next, in no particular order, I'll be working on:
- CDCL solver
- A compiler from annotated SSA to SAT
- Refactoring and improving all that with Plated

And the long-term goal: building an SMT solver.

PITAminology

Another reason why studying with someone proficient, or in a structured course, is often better: terminology.

When I study alone I tend to go with known names for the new concepts. While it works for me, it makes communicating with others PITA for both sides.

The most recent case was with the word "exemplification".

While learning to build a SAT solver I went through multiple articles and never saw this term once. Meanwhile, at work we have a part of the codebase tied to an SMT solver, and that section felt impenetrable. Writing my own solver helped, but I still kept stumbling over this word.

It turns out "exemplification" is embarrassingly simple: providing an example that satisfies the formula, instead of just saying SAT or UNSAT. I already knew the idea, I just didn't know the word. In my own pet project I even called it "solution". And that missing piece held me back far more than it should have. Once I finally learned it, that part of the codebase clicked instantly.

It might look trivial. And IT IS. But this happens a lot and is really frustrating.

Just finished reading the paper "Ghosts of Departed Proofs". I knew type-level Haskell was cursed, but I was not ready for this. It seemed fine for shorter examples, but when things get complex…

Anyways, I'll keep this short since I have a headache now: may the life of writing type-level Haskell not find me. At least not until Dependent Haskell.

JLPT N5 (6 July): Failed (62/180)
NAT Q5 (17 August): Failed (62/180)
NAT Q5 (14 September): Failed (to be updated)

Imagine going through life never playing Outer Wilds. Couldn’t be me. Your life is incomplete if you haven’t played it.

Meanwhile, I put a pause on the SAT-solver project to focus more on learning Japanese. I've written a small eDSL to practice my grammar (bunpō; 文法) skills in Haskell: bunpell.

Currently it doesn't have much and has only N5-level stuff. But I'm planning to grow it alongside my skills.

Note that if you're planning on learning Japanese you can do this too. It's a good practice and overall will serve as a great reference. However, don't look into my eDSL implementation. Don't look at any eDSL for that matter. Put together what's in your head.

76/180

Just 4 points short from the passing grade (80).