Brutal (Meta-)Introduction to Dependent Types in Agda (version 16.5.0, updated , published , created )
An introduction to dependent types and how dependently typed languages work behind the scenes, with lots of simple to moderately complex proofs, with heavy unification usage (because it’s awesome!), in Agda.
Originally made for Type Theory for Vegetables and Metamathematics seminars and later used for Functional Programming in Haskell and Proof Checking with Agda course.
Deliberately Obvious (version 2.0.0, updated , published , created )
An introduction to my knowledge acquisition and teaching-related content creation philosophies.
Draft: My Personal Exocortex Software System (version 0.20.0, updated , published , created )
Do you want to become an awesome cyborg who can easily track lots of medically, personally, and generally relevant variables, perform exploratory data analyses over them, refer back to previously experienced and related things at light speed, compute Bayesian probabilities for anything, apply the scientific method to everything, and use said abilities to optimize your life and knowledge-management? I do! This article discusses my adventures in designing, building, and growing my personal exocortex software system setup for the abovementioned purposes. It also describes how you can setup such a system for yourself.
Reinventing Formal Logic (version 3.0.1, updated , published , created )
An introduction to Hilbert- and Gentzen-style intuitionistic propositional logics, with the proofs of the deduction theorem and their equivalence, in Agda.
Originally made for Type Theory for Vegetables seminar.
Nix-, Nixpkgs-, and NixOS-related ideas (version 1.0.2, updated , published , created )
My wishlist for Nix, Nixpkgs, and NixOS features.
NixOS-install-via and related ideas (version 1.0.2, updated , published , created )
Some notes on how NixOS could be modified to make it perfectly usable on very low memory machines, like cheap VPSes.
Cybercrud and Anti-circumventiontopia: Reflections on Enshittification, EULA Roofieing, and Related Phenomena (version 1.1.0, updated , published , created )
Between 1970s and early 2000s it appeared as if we were steadily moving into computer-enabled utopia. Today, we somehow ended up in cybercrud-filled anti-utopia instead. How did this happen? What can personally you and we, collectively, do about it? This article explains how anti-circumvention and shareholder primacy laws, when applied together, degrade our whole civilization's efficiency while also making it culturally amnesiac and horrifically easy to destroy. Then, it discusses a bunch of possible solutions to these issues.
Draft: Quirks of Copyright (version 0.1.1, updated , published , created )
A discussion of history and quirks of copyright laws.
Stub: Nutrition (version 0.0.1, updated , published , created )
Mainstream nutrition claims that diets high in protein and red meat cause a bunch of metabolic issues, including kidney issues, type-2 diabetes, arteriosclerosis, and cancer. This article discusses the evidence for these claims and estimates probabilities of those claims being true by applying simple logic and Bayesian reasoning to relevant studies. The resulting analysis shows that, most likely, most of those claims are false. The only exception is the claim that smoked foods increase cancer risk, which is likely true. Which, when other relevant evidence is taken into account, points to a more general hypothesis of "ingesting products of combustion of organic matter, as part of smoked and/or deep fried foods, cigarette smoke, or anything else, increases cancer risks".
Stub: Bayesian Studies: Applying Bayesian Reasoning to Scientific Research and Analysis (version 0.0.1, updated , published , created )
You have a hypothesis and you want to know the probability of it being true. "Bayesian reasoning" note explains how to do the math. But how do you design your own study to collect data in a way that accounts for common statistical phenomena? How do you assign prior probabilities? What if you want to use published scientific studies as evidence, how do you convert p-values and confidence intervals to likelihood ratios? This article explains.
Bayesian Reasoning: Bayesian Inference with Bayes’ Theorem Extended to Multiple Tests or Pieces of Evidence (version 1.2.0, updated , published , created )
Bayes' theorem allows you to compute a probability of a hypothesis assuming a piece of evidence. But what do you do when you have several (hopefully independent) tests all pointing in different directions with different probabilities? Naively applying the classical formula of Bayes' theorem expressed using the law of total probability multiple times in a row for each piece of evidence will produce an incorrect result! The simplest way to do this properly is to switch to using Bayes' theorem in odds form, multiply likelihood ratios, and then convert back to probabilities. What? Why? This article defines everything, derives all the relevant formulas from scratch, and then demonstrates how to use them with some examples.
Why does hoardy exists? (external, updated , published , created )
“But
ZFS/BTRFSsolves this!” I hear you say? Well, sure, such filesystems can deduplicate data blocks between different files (though, usually, you have to make a special effort to archive this as, by default, they do not), but how much space gets wasted to store the inodes? Let’s be generous and say an average inode takes 256 bytes (on a modern filesystems it’s usually 512 bytes or more, which, by the way, is usually a good thing, since it allows small files to be stored much more efficiently by inlining them into the inode itself, but this is awful for efficient storage of backups). My home directory has ~10M files in it (most of those are emails and files in source repositories, and this is the minimum I use all the time, I have a bunch more stuff on external drives, but it does not fit onto my SSD), thus a year of naively taken dailyrsync-backups would waste(256 * 10**7 * 365) / (1024 ** 3) = 870.22GiB in inodes alone. Sure,rsync --link-destwill save a bunch of that space, but if you move a bunch of files, they’ll get duplicated.In practice, the last time I deduplicated a never-before touched pristine
rsnapshothierarchy containing backups of my/home/oxijit saved me 1.1 TiB of space. Don’t you think you would find a better use for 1.1TiB of additional space than storing useless inodes? Well, I did.
Why does Hoardy-Web exists? (external, updated , published , created )
“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!
UNIX in 1970s had better system backup tools than current Android OS (external, updated , published , created )
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.
Isn’t GMail good enough? (external, updated , published , created )
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.
Your emails will eventually get stolen anyway (external, updated , published , created )
(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.)
How to Learn Functional Programming and Type Theory (version 1.0.1, updated , published , created )
This entry is the second one in a series of blog posts about Agda. It describes the most boring method of learning something called "functional programming". The method is designed to be a fast way for people with perseverance (and masochistic propensity) or background in maths and/or computer science (and a hard humiliating way for everyone else).