Posts

You are filled with determination… Doing proofs from the book Programming Language Foundations in Agda in the Lean 4 prover has really been a refreshing experience for me. However, things did get annoying sometimes for me, especially when I just couldn’t get pass the termination check. Although I haven’t seen every piece of the puzzle yet, I do hope that by sharing what I have seen so far, this blog post could save you some time from bashing “lean termination” into your search box , which could potentially lead you to some random web pages about Lean Manufacturing....

Now playing: Bad Apple!! Problem Being a polyglot can be painful sometimes. Particularly, it is extremely common for me to have multiple windows open at the same time, each using a different language: at this very moment, I have my messenger on where I participate conversations in Chinese, and I am writing this post in English at the same time in my VSCode window. As a result, with OS defaults, I have to switch between input sources (a....

Hi there! I have been using GitHub repos as my scratchpads since my very first days as a self-taught developer. However, it did occur to me recently that I could use some more organized form of output. Hopefully, this blog will help me take notes of my random ideas and efforts while providing the right contexts for them, so that they might not remain undiscovered lying in my repos. À très bientôt!...