Hey, guys. It is a second try of my blogging. You know me from my prev. channel and if you don’t know me, it is not a problem, just read my posts. You are here to learn something, not for deanonyming me. Let’s start 😀

Hey. in these days, I started to learn "Lean 4" in parallel while I am learning Haskell. Here my first simple proof you can see:

example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
  rw [← mul_assoc a b c]
  rw [← mul_assoc b a c]
  rw [mul_comm a b]

In these example, I proved a * (b * c) = b * (a * c) with multiplication association and commutative properties.

1. I rewrite expression on the left with association: a * (b * c) -> a * b *c
2. I rewrite expression on the right with association: b * (a * c) -> b * a * c
3. I rewrite expression on the left with commutative for a and b: a * b * c -> b * a * c
4. Expressions on the left and right now equal with reflexivity: b * a * c = b * a * c

Link

In this problem, you have to implement your sqrt function without using any std library.

What did I do? Using a property of sorted order of natural numbers, I did binary search between 0 and half of given number. And checked square of mid number is equal to given number. If result is not found, returned the last number which square of this number is less than given number

Yesterday, we have participated in Cyberkent 3.0 and have got 20 place.

It is nicer than previous year

In our infrastructure, there are workers with single instances and if you start multiple pods over k8s, you will have only one, single instance of worker. It is like you are using single cpu core to render your game instead of 16 cores.

So, I researched internet and learnt a new way of distributing jobs over multiple workers. To do that, you have to be planners, partitions and workers. And here we go! We can distribute our jobs across k8s multi-pods.

Here, you can see example (non-working) of this approach: https://gist.github.com/abdivasiyev/ad958dba544daa8fc59c5d59781d55ce

Workers are simple event listeners of MQs.

starting all containers using a single command:

docker start $(docker ps -a --format=json | jq -r .ID)

stopping all containers using a single command:

docker stop $(docker ps -a --format=json | jq -r .ID)

Starting of the Monday, I am officially on a holiday for 1 week.

Plans:

- Close laptop
- Shut down phone
- Sleep
- Go outside
- Do something enjoyable

🥴🥴🥴

Article

Red black tree implementation in Haskell (repo link)

Linear Haskell

https://dl.acm.org/doi/pdf/10.1145/3158093

Linear Types Proposal in GHC

https://ghc-proposals.readthedocs.io/en/latest/proposals/0111-linear-types.html

Garbaga collecting on Haskell

Entrypoint: https://gitlab.haskell.org/ghc/ghc/-/blob/master/rts/sm/GC.c#L282

https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/rts/storage/gc

Finally, I could configure nix development shell with proper LSP support for Go compiler. It was not easy as a beginner nix user. After 4-5 hours researching I decided to see nixpkgs.go_1_25 package and got frustrated from that. Because it was an easy task 😮‍💨

Anyways, I did that! And I am ready to contribute some Go code. Now I am looking through issues page to find easy one to start

https://gist.github.com/abdivasiyev/792939fc4d961b4ad049e7ebb8d8bcf8

Advent Of Code 2025: Day 1

https://github.com/abdivasiyev/aoc-haskell/blob/aada93c69659b71e994248cbae0ecdc1c647fdd4/src/Aoc/Years/Year2025/Day1.hs

Working in a team is nightmare for an introvert people like me I think. Just I want to work in a quiet without any questions, but it is not possible 😥

Advent Of Code 2025: Day 2

https://github.com/abdivasiyev/aoc-haskell/blob/master/src/Aoc/Years/Year2025/Day2.hs

AoC Day 3 Part 2 is so crazy

A few days ago, I had to use sqlc to generate Go code from sql queries and there was a lack of overriding named parameter types. So I couldn't do anything without it. And after some research I saw sqlc's plugin system and understood how to add my custom overridings. And it was a usefull. Now I am writing only sql queries to generate my repository layer.

https://github.com/abdivasiyev/sqlc-gen-go/commit/c65fe5fa9f63528a46af3cfcc7ec833677bfac46

now my neck is resting finally