Write-ups that were not peer-reviewed or which are less structured than papers.
↑ (v. 3.0.0) ⊩ Reinventing Formal Logic (created on , published on )
Have you ever wondered why there is the deduction theorem which is a theorem, yet implication introduction is an axiom?
Obviously, the answer can be deduced from the [referenced] Wikipedia articles. But it’s much more interesting to find it the hard way. Let’s reinvent basic formal logic ourselves!
Originally made for Type Theory for Vegetables seminar.
↑ (v. 16.3) ⊩ Brutal {Meta}Introduction to Dependent Types in Agda (created on , published on )
Nevertheless, I think it is the hard parts that matter, and I always wanted a tutorial that at least mentioned their existence (well, obviously there is a set of dependently typed problems most people appreciate, e.g. undecidable type inference, but there is still a lot of issues that are not so well-understood). Moreover, after I stumbled upon some of these lesser known parts of dependently typed programming I started to suspect that hiding them behind the language goodnesses actually makes things harder to understand. “Dotted patterns” and “unification stuck” error in Agda are perfect examples.
Originally made for Type Theory for Vegetables and Metamathematics seminars and later used for Functional Programming in Haskell and Proof Checking with Agda course.
↑ (git) ⊩ Why does Hoardy-Web exists? (created and published on )
“If it is on the Internet, it is on Internet forever!” they said. “Everything will have a RESTful API!” they said. “Semantic Web will allow arbitrarily complex queries spanning multiple data sources!” they said. They lied!
↑ (git) ⊩ UNIX in 1970s had better system backup tools than current Android OS (created and published on )
Or: “How Google screwed up Android backups, apparently on purpose.”
This also resulted in usefulness of
adb backupitself being reduced because in Android version 6 Google made automatic daily file-based backups that get uploaded to Google the default when you attach your phone to your Google account. So, most apps started to opt-out of those backups for privacy and security reasons – which also started opting them out of being included inadb backupoutput, sincebmgrandbushare most of the infrastructure. Some of those apps now implement their own in-app backup buttons hidden away in the settings menu somewhere, but most do not.
↑ (git) ⊩ Isn’t GMail good enough? (created and published on )
Today, Google provides email services for free, and so >70% of all e-mails originate from or get delivered to Google servers (GMail, GMail on custom domains, corporate GMail). Now it’s Google who decides which messages you get to see and which vanish into the void without a trace.
Which, as a recipient, is highly annoying if you frequently get useful mail that GMail marks as spam or just drops (happens all the time to me). And, as a sender, is highly annoying when you need to send lots of mail. Just go look up “Gmail Email Limits” (on a search engine other than Google). It’s a rabbit hole with lots of ad-hoc rules on just how much mail you can send before GMail decides to just drop your messages, yes, drop, not mark as spam, not reject, they will drop your mail and tell neither you nor the recipient anything at all.
Moreover, they are now working towards making their
INBOXinto an algorithmically generated feed with “important” messages being shown first. It’s easy to see where this is going.
↑ (git) ⊩ Your emails will eventually get stolen anyway (created and published on )
(Seriously, abstractly speaking, I’m kinda interested in civilization-wide legal and cultural effects of every embarrassing, even slightly illegal and/or hypocritical thing every person ever did relentlessly programmatically exploited as blackmail or worse. Non-abstractly speaking, why exactly do governments spend public money to make this possible? After all, hoarding of exploitable material that made a disaster after being stolen worked so well with EternalBlue, and that thing was a fixable bug, which leaked blackmail is not.)
↑ (v. 1) ⊩ Misc Nixpkgs/NixOS-related project ideas (created and published on )
Various other ideas towards improving Nixpkgs and NixOS.
↑ (v. 1) ⊩ NixOS-install-via (created and published on )
Design ideas for a better nixos-install utility.
This page is going to replace the blog, eventually.