What is it The other day I learned about TLA+, PlusCal, and Quint. TLA+ is a formal specification language that can be used to design, model, and verify software systems. As the name suggests (TLA: Temporal Logic of Actions), it is particularly well suited to describing state transitions and behaviors over time.
PlusCal is an algorithm language that is normally written inside a comment in a TLA+ module. Its syntax is more familiar to programmers who are used to imperative languages. The PlusCal translator converts it into TLA+, which can then be checked with the TLA+ tools.
Omarchy Tokyo Meetup vol.1 was held on Thursday, September 10 at KOMOJU in Kichijoji, Tokyo. I took part both as the venue host on the KOMOJU side and as someone who wanted to learn more about Omarchy.
Slides from the talks #omarchy_tokyo on X This was the second Omarchy Tokyo meetup. The first one (vol.0) had around ten people, and we spent the time installing Omarchy on our laptops, which was fun in its own way. This time there were more than thirty attendees, plus pizza and drinks courtesy of KOMOJU, and nine speakers covered a wide range of topics: Omarchy Quattro, plugins, window managers, KVM, Japanese input methods and fonts, UMPCs, and how people actually use Omarchy day to day.
Today I learned about age. This is a turnkey file encryption format and tool/library that uses hybrid encryption. Unlike PGP, it is specialized for file encryption.
Quick hands-on steps:
# 1. Create a secret file echo "The king has donkey's ears." > secret.txt # 2. Generate the key pair age-keygen -o key.txt # 3. Encrypt the secret file age -r <PUBLIC_KEY> -o secret.txt.age secret.txt # 4. Decrypt the secret file age -d -i key.txt secret.txt.age Instead of generating a new key pair with age like the above, an SSH key pair, or even a passphrase can also be used for encryption/decryption.
I attended JP_Stripes Connect 2026 at Information Science College in Yokohama on Saturday, August 1. The theme was “Find out how to monetize in the AI era.” The event had two tracks: main and tech. I’m basically a tech-side guy, but this time I stayed on the main track throughout the event.
I couldn’t arrive at the venue in time for the beginning of the keynote session by Daniel Heffernan, but I was still able to learn how frequently prices are changing these days. One well-known online service changed its pricing ten times within a single year. The session explained that pricing is a product（価格はプロダクトである）and encouraged companies to keep iterating on it based on what they learn.
Recently I learned about PTA: Plain Text Accounting. You can record income and expenses with plain text, gather data programmatically, then calculate and visualize. Ledger, hledger, and Beancount are software tools that provide a way to express double-entry bookkeeping in plain text. They use similar plain-text DSLs, though Beancount is not directly source-compatible with the others.
Here’s a small example of Beancount syntax (Assume these accounts were opened earlier):
2026-08-03 * "Employer" "Salary" Assets:Bank 300000 JPY Income:Salary 2026-08-04 * "Cafe" "Coffee" Expenses:Food 600 JPY Assets:Bank What does it mean PTA provides a shared style of notation for expressing accounting activities in plain text. This is handy common knowledge in case we want to write down transactions quickly in a text file or even on a whiteboard. Similar to the benefit of UML.
