Amélia Liao 🍊😈

Main author of the 1Lab, maintainer of the Mikan proof assistant, and more online than you. Charitably describable as "hinged"

Public Key

npub105djthvncz3tms6ke37w4579d0qqmf2e6xt9p7z5h3ayq0wtq7pswyvwnw

NIP-05 Address

amy@types-pl.mostr.pub

Profile Code

nprofile1qqs86xe9mkfupg4acdtvcl8260zkhsqd54var9jslp2tc7jq8h9s0qcpz4mhxue69uhhyetvv9ujuerfw36x7tnsw43qqdt848

Publishing to

relay.ditto.pub

Author Public Key

npub105djthvncz3tms6ke37w4579d0qqmf2e6xt9p7z5h3ayq0wtq7pswyvwnw

Show more details

Last Notes

2026-10-21 10:00:04 UTC

you...!!
https://pool.jortage.com/typespl/media_attachments/files/117/478/311/374/045/305/original/91ba608eb817efc1.png

2026-10-08 10:11:02 UTC

the reason your body temperaure goes up when you're sick is that the viruses are using your body to mine crypto

2026-09-27 17:47:15 UTC

if scientists cared about advancing humanity they would be researching a way to reheat crispy foods without them going soggy

2026-09-26 14:33:56 UTC

eagerly waiting to find out which neurotransmitter is going to ascend to the rank of fourth modern humour together with dopamine, serotonin and cortisol

2026-09-24 13:08:05 UTC

aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa
#nevent1q…jdz5

2026-08-01 04:35:29 UTC

this seems really depressing until you think of all the shareholder value we generated
#nevent1q…mkfy

2026-07-15 11:13:33 UTC

when a technofascist oligarch says their new toy is inevitable, you must remember that what they mean is that your rejection of that toy would decrease their potential earnings.
when anyone else says a new technofascist toy is inevitable, you must remember that what they mean is that they are comfortable with "cattle" being their station in life.
neither of these assertions are an actual truth about reality. neither forms sufficient justification for adopting something.

2026-06-26 12:22:17 UTC

For a long time my birthday has been a pretty depressing time: even here in the tropics 🏖️🌴💃 June is a cold and dry and dreary month with short ass days where nothing gets done, and this does not help process the previous year in an objective light. For, like, a decade running, it has only felt like I'm tallying up another year spent stagnating.
But this year, for a change, I do have a project that feels meaningful. However small its impact may turn out to be, I feel like I am doing something that matters, and that I am doing the right thing. And even through my depression I can be proud of that

2026-06-18 17:30:41 UTC

In light of recent discussions (and the passage of time), I've decided to update the Mikan FAQ.
Changes to note:
The "what's been happening?" question has been updated to reflect the new interesting work that has been getting merged!
The "will Mikan support book HoTT?" question from the original FAQ turned out to have been, like, at least two different questions, and so in twain it has been splat. The new questions should hopefully clarify the fate of the language flags, computation (or lack thereof) with indexed inductives, and maybe even why all your lambdas are yellow.
Until we work out a good story for authoring and deploying Mikan documentation, the FAQ will live in the 1Lab, but the link above goes to a preview page. In other news, we're just about ready to merge the porting effort! Believe it or not, we did actually make use of a bunch of features we decided on axing.

2026-06-15 00:50:10 UTC

something the physicists won't tell you is that if you add enough bodies it becomes real easy to calculate their orbits as the entire system decays into a black hole

2026-06-03 16:22:54 UTC

drivin to work in my Toyota Corollary

2026-05-27 23:54:01 UTC

beware: your consequences might have carequences and cdrequences

2026-05-26 14:11:32 UTC

how it feels to be responsible for the termination checker
https://pool.jortage.com/typespl/media_attachments/files/116/641/274/432/698/687/original/2ca4619a74ece10d.png

2026-05-05 13:40:43 UTC

We're announcing Mikan: a proof assistant for cubical type theory, forked from the Agda codebase.
Note: you can also read this announcement as a Gist.
The Agda developers have recently proposed codifying their official stance on LLM-generated contributions: they are "concerned about the negative effects of large language models (LLMs) on many individuals, our society, and our planet", but refuse to take any concrete action to address their own contribution to these. They have judged the hypothetical future usefulness of the slop generators as outweighing the present, very real harm being caused by the AI industry.
We understand that, over its 20 years of Git history, Agda's implementation has evolved to cater to subsets of its user-base with very diverse, and often conflicting, needs. However, the attempts to bridge these divides (e.g. --without-K vs. --cubical-compatible) present a significant maintainership cost, and are often resented by both camps, since they present one camp with substantial performance costs, while offering the other camp no clear benefit, since code across the divide is written with very different formalisation sensibilities.
Other extensions to the type theory are kept despite known inconsistencies (sized types), or being impossible to adopt without complete vertical buy-in (cumulativity, erased cubical), or simply for backwards compatibility (--guarded/@lock). In the best cases, these features are championed by a single maintainer, and keeping them well-tested against the continuous adoption of new features is a struggle when very little code uses them.
Our plan is to focus on exactly one variant of the language ("full --cubical"), and to drop support for all the language features which are explicitly deprecated, inconsistent, or simply ill-understood in conjunction with this fragment. This will give us a solid base from which we can work to improve the experience of working on the Mikan codebase, to attack the existing correctness and usability issues with features like termination and positivity checking, and to pursue breaking improvements to the core type theory and its user interface.
Signed:
Amélia Liao (@nprofile…ktlj)
Naïm Favier (@nprofile…2p65)
Reed Mullanix (@nprofile…pkkx)

2026-04-20 08:51:56 UTC

gasp. i'm shocked. this is my shocked face: 😐
#nevent1q…5385

2026-03-22 11:42:18 UTC

here's a cursed trick that i should probably write up as a blog post but writing for my blog is super hard for reasons i don't comprehend (probably having to use uppercase letters).
if you've tried to do anything with monoidal categories or (as pictured) bicategories in Agda you will probably be aware that getting the goals to print nicely is. an uphill battle. for example, attached is the inferred type of the pentagon axiom. setting aside that the variable B has been renamed in the telescope (i already have a B in scope), there are several problems:
all types of 1-cells are printed as Hom.Ob, with no indication of whence or where they're going. also, the associator is printed as associator.from .η instead of α←.
the 1-cell composition and horizontal 2-cell compositions are printed as compose.F₀ (f , g) and compose.F₁ (f , g).
problem one is actually very easy to address without changing the definition at all. the relevant feature here is something called display forms. agda definitions (including, as in this case, projections) can have bits of metadata attached, consisting of a pattern and a right-hand-side term, which cause the reification pass to print a neutral headed by that definition as something other than an application of that definition.
when you have a module application module Y = X α in scope, agda automatically attaches display forms to (the normal forms of) definitions x from X saying that, if they are applied to the parameter(s) α, they should be printed asY.x, instead ofX.x α, and this applies *regardless* of how you got your hands onX.x α`. for example:
module X (A : Type) where postulate foo : Type
open X Bool renaming (foo to bar)
_ = {! X.foo Nat !} -- normal form prints: X.foo Nat
_ = {! X.foo Bool !} -- normal form prints: bar
so now if you look at the 1lab definition of Bicategory as it was last week, you can spot the problem: the type a ↦ b of 1-cells was just defined as a function, which does not get automatic display forms, and there was a module application of Hom in scope through which you could access Ob without parameters. the first part of the fix is to prevent Ob from being accessible through the copy without parameters:
module Hom {A B} = Precategory (Hom A B)
hiding (Ob)
for the second we need a cursed incantation to work around record definitions allowing module copies but not module bodies before the last field:
private
open module ↦ A B = Precategory (Hom A B)
public using () renaming (Ob to _↦_)
the private declaration applies to the definition of module ↦, but not to the open … public, so the definition _↦_ is still exported. we've now defined _↦_ : Ob → Ob → Type _ entirely through the module system, so we get a display form saying that B .Prebicategory.Hom X Y .Precategory.Ob should be printed as Prebicategory._↦_ B X Y, which doesn't look like an immediate improvement, but this rule "stacks", so if you have a local module B = Prebicategory B, you'll see X B.↦ Y instead. if we apply this trick also to the coherence maps, you get the second version, which is a marked improvement.
but even in the second version, the composition operator(s) print prefix: ⊗.F₁ (Hom.id , α← (g , h , i)). unfortunately, there is no way to uncurry a function (here the F₁ field of the composition functor) using the module system only, and user-written display forms can't match on neutral projections, so this is as far as the improvements go without changing the types of the fields that go into a bicategory.
for the longest time i have known what the solution was: change the definition of Bicategory to be in terms of an "atomic" definition of bifunctor, instead of having composition have type [ Hom B C × Hom A B , Hom A C ]. but this sucks, for a variety of reasons, so i didn't want to do it. however. if you have a friend whose brain is in the "on" position more often than mine (for me, that was @nprofile…pkkx), they might point out that if you transpose that to [ Hom B C , [ Hom A B , Hom A C) ] ], the actions of the composition functor basically take two arguments. so you might wonder: can we define those entirely with the module system? and the answer is yes!
if you have a Functor C Cat[ D , E ], these arcane sigils project out the action on objects as a two-argument function, and the actions on morphisms in each side as a pair of whiskerings that take both the morphism to act with and the object that isn't changing: A ▶ f and g ◀ B, as written there, but you can use another symbol. and by redefining bicategories to take one of these instead, we can get the normal form(!!) of the inferred type of pentagon to print as written (modulo the renaming to avoid B again, sigh).
this isn't a completely painless refactor, since it changes the primitive 2-dimensional operator from horizontal composition to a pair of whiskerings, but it is super doable (we're in the process of doing it), and also super worth it. it also breaks less than you might expect: just this last week we got a drive-by pull request adding a solver for equations in bicategories, basically a practical version of the coherence theorem, which feels like something that would have to be completely rewritten to account for this change, right? not right! it was a ± 30 diff to get it working, and most of that was from having to split the whiskerings in the syntax.
https://pool.jortage.com/typespl/media_attachments/files/116/272/460/646/539/146/original/063dc6bd68dc851d.png
https://pool.jortage.com/typespl/media_attachments/files/116/272/564/238/409/216/original/a506f3863a16d76c.png
https://pool.jortage.com/typespl/media_attachments/files/116/272/592/433/552/145/original/5aba89128f5ef8b2.png

2026-03-13 09:30:31 UTC

- reply

if you are a snake arguing against such a policy, please do the polite thing: puff out your chest, and yell out for all to hear, "I LOVE THE TASTE OF BOOT". do not waste the time of those who might have cared about your project by hmm'ing and haw'ing.
also please come forth under this post so i can block you already. you worm

2026-03-13 09:27:25 UTC

a policy enforcing a blanket ban on contributions made with the use of LLMs is not, actually, 'mandating ideological purity'. it is, in fact, the bare minimum to ensure that your project won't be treated as completely radioactive by anyone with morals.
moreover, do not let anyone supporting Appeasement for sam altman and his ilk distract from the point at hand by trying to argue that the use of LLMs is in some way equivalent to choosing a license which allows the project to be used by e.g. defence contractors (i.e., any actual open-source license).
only one of these burns the reputations of those in the commit log to manufacture consent for the slop salesmen.

2026-03-10 09:37:30 UTC

look at my stupidly photogenic cat
https://pool.jortage.com/typespl/media_attachments/files/116/204/203/717/798/588/original/481d45f590383113.jpg

2026-02-17 13:14:28 UTC

people sometimes talk about proof assistants being like games so lets take that literally if we can't match the interaction points across an edit in vscode we'll just queue a song and pop up the taiko UI and on each beat have the user click a {! !} token in their file to associate it with that interaction id
click the goals to the beat

2026-02-12 12:17:16 UTC

ive got a simple solution to the acms financials which is send all the extra money to me personally and then fuckin disincorporate or whatever. stop existing

2026-02-07 13:42:12 UTC

trying to make your type theory 'more convenient' by shoving things into the definitional equality reminds me: a while ago there was a proposal to extend cubical agda with a hierarchy of universes of strict n-types, like arend.
this is a fantastic idea. if you hate yourself. just like strict prop results in something that looks a lot like the ((-1)-connected, (-1)-truncated) factorisation system (a.k.a. (epi, mono)) but mathematically stunted by the necessary inability to prove that a family is strictly (-1)-truncated, an infinite hierarchy of universes of strict n-types results in your type theory being littered with Utter Dogshit versions of the (n-connected, n-truncated) factorisation systems for every n! truly, an incredible development

2026-01-28 15:32:25 UTC

i am being lectured on good agda architecture by a crackpot high on the fumes of the money they burned on claude tokens

2026-01-26 07:47:59 UTC

my Agda 2.9.0 features: record where, qualified do, qualified idiom brackets, new conversion checking errors, info buffer go-to-definition, parallel type checking

2026-01-21 23:09:54 UTC

casually cuts your type checking time by two thirds https://github.com/agda/agda/pull/8332

2025-12-22 12:10:34 UTC

what does literate programming for a forest look like

2025-12-20 12:36:42 UTC

- reply

@nprofile…w8t5 @nprofile…rrqe Actually, it is MLTT! See, like, §4.1.3 in Jesper's thesis. It shows how to automatically construct an equivalence between true ≡ true and ⊤, without K, and then §4.3 shows you how to deploy that equivalence to translate the pattern-matching function you wrote to one in terms of nothing but eliminators while preserving all the clauses you wrote as definitional computation rules. There is no bug here. There's barely even a feature request here, since you've already lobbied for --no-pattern-matching in the past. I don't want to commit to supporting twelve other feature flags for whatever unification step you feel unhappy with on a given day. You know these functions all rely on the exact same behaviour, right? Why isn't this file called MLTT.Wrong-Vector?

2025-12-20 11:57:10 UTC

- reply

@nprofile…w8t5 @nprofile…rrqe … it's not a bug that constructors for (non-higher) inductive types are disjoint and injective. in fact this is like agda's most sensible feature

2025-12-13 22:39:01 UTC

- reply

@nprofile…rrqe make sure NOT to tell any of the developers and conspiracypost on maths reddit

2025-12-13 16:08:06 UTC

- reply

@nprofile…rrqe it's the only thing i've written that people, unprompted, thank me for 😆

2025-12-12 11:50:54 UTC

yeah i do find that hard to believe
https://pool.jortage.com/typespl/media_attachments/files/115/706/445/371/396/963/original/32fa6a59b3d699ac.png

2025-12-02 13:21:48 UTC

- reply

@nprofile…rrqe In general I think the state of the art in unification with unique meta solutions isn't ready for strictly associative operations 😅 It hasn't been a problem for us. In fact, we define the monadic operators in ↯ by copattern matching, and ↯ itself is a no-eta record, which allows _>>=_ and friends to be definitionally injective in the arguments. I think allowing eta-expansion to expose the shape of the underlying proposition and "continuation" would probably lose this, even if these match 1:1 the tree of monadic operations.

2025-12-02 12:28:57 UTC

- reply

@nprofile…rrqe have not thought about it as much. (i've only really thought about this problem for PCAs, where that would be a very strange thing to ask for).
from a code reuse perspective, i think it'd make the most sense to allow fields to concretely specify an implementation of the inverse operation, constrained so the extent is equivalent to apartness from zero (or whatever). then in the case of a discrete field we can simply have the extent compute by cases on the denominator to either the unit or empty types.
tbh, even in the discrete case, i think it's somewhat strange to make inverses a total operation, since you still need to prove things are actually invertible when it comes to reasoning about them. i think keeping it as a "self-deciding" partial operation strikes a good balance between "i have to be honest when reasoning in context" and "i can ask the proof assistant to just normalise a number in anger", since if you're not normalising a stupid number the extent of any combination of field operations will have computed to a big tuple of unit values.

2025-12-01 18:19:18 UTC

- reply

if you don't have a small Ω to build a size-preserving ↯ with then (a) i'm curious how much you care about that anyway, with since your ℝ is either not going to be very nice, or going to be large anyway; (b) i'm pretty one can build the initial dominance containing every proposition x ♯ 0 for x : ℝ by higher induction-induction in the same manner as the HoTT book reals, or more simply by higher induction-recursion, and that's all you need to apply this particular trick here.

2025-12-01 18:12:05 UTC

if you ask me what to do about the division operator in non-discrete fields my honest opinion is that in any algebraic-adjacent structure with a partial operation, the very first thing you should do is ditch the actual underlying type 𝔽 of that structure completely, and work entirely in partial elements ↯ 𝔽, just like we do for PCAs in the 1lab.
sure, now all your equational lemmas end up looking like "if a is defined and b is defined then a + b is b + a", but you're not indexing anything over those proofs, so they barely matter. which means you can apply whatever automation you want. of course, if you're not inverting anything, the proof will be a big tuple of unit values, so you literally don't even need to write it: unification and eta expansion will get you the unique solution. if you are inverting something, you'd need to cough up that proof whenever you want to apply an equational law even if you believe in santa, because whatever junk value you map an undefined inverse to is not actually an inverse.
since the proofs are not guaranteed to be definitionally irrelevant (hell, the evidence that a real number is invertible is basically just the inverse), to make sure they stay out of the way, even in the case you're looking at a defined thing, you don't ever project it back onto 𝔽. instead, if you need to put an 𝔽 in a record or something, you work with the image of 𝔽 in ↯ 𝔽, i.e. the type (p : ↯ 𝔽) × ⌞ p ⌟. basically, if you find yourself writing a type family over 𝔽, just. don't. what you want is instead a type family over ↯ 𝔽 which implies its argument is defined.

2025-11-18 16:54:10 UTC

semantics is concrete, syntax is a semantics, computer science is a mathematics

2025-11-17 18:55:09 UTC

- reply

@nprofile…rrqe have you seen the 1lab proof? actually pretty easy to show directly that Ω S¹ satisfies (enough) of the universal property of the integers to get an equivalence. though i guess transferring this to book hott is what one might call gnarly

2025-11-15 14:59:23 UTC

definition. an anaesthetic is a substance which has the function of negating aesthetics

2025-11-15 11:50:06 UTC

- reply

if elaborating a definition mutates a global symbol table to insert the defintion you've lost and will have to live with the consequences of your shitty design (e.g. people can't implement sensible implementations with great performance wins because you have to work around your elaborator being extremely slow (for unrelated reasons) by glorified attempting to find the first line that didn't change and reusing that snapshot of the global mutable elaborator state) forever

2025-11-15 11:48:05 UTC

if i were implementing an elaborator it would be completely stateless outside of metavariables which are ofc local to a binding-group

2025-10-28 17:02:38 UTC

re. whats been going around recently if theyre type theorists theyre not gonna be using Lean
https://pool.jortage.com/typespl/media_attachments/files/115/452/867/075/476/166/original/b55e593383ef65fa.png

2025-10-16 17:16:40 UTC

every function decomposes its domain into a sum (in the biz we call this path induction)
it's a lens if that sum has all factors the same, so the decomposition is into a product

2025-10-07 00:21:06 UTC

there is a simple sensible solution to overloading which is to get rid of it and then allow qualifying any expression by a module

2025-09-30 11:13:53 UTC

- reply

@nprofile…6kk0 oh yeah if possible I would keep the full de morgan structure but if I met the devil at a crossroads and she told me I can have either connections or reversals I'm pretty sure I'm picking the reversals

2025-09-30 10:31:15 UTC

it's annoying that reversals are presently problematic because honestly i'm down to drop the connections but having the reversals makes everything so much easier

2025-08-28 05:22:19 UTC

i find univalence appealing because it greatly increases the amount of things i can not care about. definitional proof irrelevance— and this includes the limited case of definitional UIP— is appealing at first because now there are things you totally don't have to care about, but in reality it forces you to care extra hard about so many more things, even at the set-level, than you would have to had you gone for a proper, semantic notion of proposition.
as an example, inverses in a group are unique, but not in general not definitionally so, so if all your infrastructure for not caring about things is built around strict propositions, you have successfully conned yourself into caring about you shouldn't have to (especially if you're trying to beat a system for inferring properties into coming up with something you've made into structure... 💎). and sure, you could put the inverses behind a truncation, so now they totally don't need caring about... but everyone agrees that would be silly, right? since that's a strict truncation, there's no getting out of it, not without implying full equality reflection. it wouldn't be unjustified to postulate unique choice, and use that to "get back" an inverse-assigning map, but... that's not gonna compute. regardless of how concrete your group implementations actually are.
mathlib is extremely concerned with the distinction between finite-products categories and cartesian monoidal categories. to a comparable extreme i do not want to care about that. any theorem of category theory is insensitive to the set-theoretic identity of your product-assigning map. you should not need a truncation here. if you ask me, the observable difference between "having products" and "being equipped with an operation that assigns products" on strict categories speaks to nothing more to the pathology of any foundation that insists on K.
(as a note, a category having products is exactly analogous to a semigroup having identities: they needn't be preserved by arbitrary maps but they are preserved by all the invertible maps, in the appropriate sense.)
to be clear, for this latter example, even if you've moved past not-caring being an artificial syntactic thing you have to choose ahead of time, even if you know how to not-care about things that happen to be unique, at the set-level, you're still boned! there's not many univalent categories to go around when that necessarily implies that objects have no automorphisms, and uniqueness of limits, like other cases of structure identity, genuinely needs univalence— not only do you need to turn an iso into an identification, you have to show that this identification takes the iso to the identity.
and all of that is setting aside the actual no-go theorems like in section 8.2 of "A Cubical Language for Bishop Sets" that, and i hope i can get away with this paraphrasing when i know all the authors on here, imply (a) the ad-hoc purely syntactic notion of strict proposition is Bad, Actually (b) these end up in an utterly privileged position in your type theory, e.g. only strict can propositions have effective quotients, so everything gets Worse, Actually

2025-06-11 00:33:06 UTC

i love brazilian product packaging law because you have to specify that your claims are really generic. so like if you write "gluten-free eggs" on the box you are allowed to do that but it has to be
"gluten-free* eggs
* like all eggs"

2025-05-26 06:46:11 UTC

- reply

@nprofile…6kk0 the dark side of the force is a pathway to many appliances which some consider to be... unnatural.

2025-05-20 15:02:01 UTC

if you have a function f : A → B between types of arbitrary h-hlevel what do you call one of the many inhabitants of ∀ x y → f x ≡ f y → x ≡ y — literally that type, without any other conditions imposed?

2025-05-19 00:22:38 UTC

so cool how if you're hungry and you eat, you're no longer hungry. imagine if that worked with sleep

2025-05-08 20:35:44 UTC

the new pope has a b.sc. in maths which i suppose as the head of the catholic church it's good that he has a solid understanding of cardinals

2025-04-26 01:12:04 UTC

what is the coolest species name?

2025-04-03 06:52:10 UTC

i don't know where to ask this question but like what happened after the k-pg extinction to select for mammals instead of like another clade of lizards

2025-04-02 08:57:34 UTC

i just saw someone recommending to learn haskell, to, quote, "become a better programmer as a side effect" - but i thought we were against those?

2025-04-02 08:00:05 UTC

so uh given that my formal writing style is basically what all the llms copied how exactly do i write a cover letter that wont get summarily dismissed

2025-03-24 12:12:50 UTC

Quillen has through his entire life and career only proven one theorem labelled A. apparently.

2025-03-01 14:05:03 UTC

- reply

@nprofile…6al5 i think my "favourite" child of this nonsense is the syntax for giving an ocaml function a polymorphic type signature (i probably have to specify — in an ml file), which does not have any overlap with the syntax for type variables, at all.

2025-02-14 08:58:31 UTC

i think the funniest thing is the phrase "neo-Marxist class warfare"... lol. is there anything more paleo-marxist than class warfare? like that's old school

2025-01-28 12:23:43 UTC

newcomers to cubical type theory complain about the lack of definitional reduction for beta on paths and to that i say the other day i wanted to do something with inductive identity and i had to prove an intermediate goal that boiled down to moving sym into thrice iterated ap because a dependent identification wasn't correct otherwise and like im from now on refusing to believe that anyone who thinks J-refl is worth having to thread all these ridiculous structural rules by hand is arguing in good faith

2024-11-14 13:37:17 UTC

In retrospect, dropping out of undergrad was a bad decision, given that the sweng job I held for a year sucked ass, and it's (probably) totally shot my chances at an academic career. But it was the only choice I had!
I reckon just about everyone was in a pretty bad place in 2022, but I was doing bad bad. Not to get into the details, but the psychiatrist I went to (for my ADHD!) had me sign a liability waiver after I chose not to be admitted. So I wasn't exactly in the headspace to think about my future even five years on when I chose to drop out.
There's no way to write this paragraph without it sounding like bragging, but, like, I've always been pretty good at computering. I picked up programming at 7; I have blog posts about Haskell nonsense from when I was 14; and the year after I implemented a compiler for a typed functional language that grew to support most of GHC's complicated extensions(*). There was no shot I was failing any of my undergrad classes.
But that didn't matter! First semester, we had to take what amounted to an intro to programming class, that was taught in Python. I talked to the professor about testing out of this class, and he said something like "I understand where you're coming from but you'll have to talk to the coordinator". And so I did! After a few more escalations, the person in charge of all the science and engineering degrees told me that they legally aren't allowed to let me test out of the core curriculum.
That was in 2020, so the week after I went through the entire circus, we switched to remote lectures. And then even though I was nominally having to spend something like 18hrs a week having someone badly explain me something I already knew, I could just mute my browser and play osu! instead. It was a tolerable two years of picking up exciting knowledge about, like, for-loops and state machines and and proofs by induction and the same amount of SQL you'd pick up from w3schools.
But then we went back to physical lectures. One of the classes for that semester was functional programming. I attended the first lecture; we were to use a version of GHC which had had a minor bug fixed by me. It was too much. With a friend's recommendation I applied for a job at Obsidian Systems, a Haskell consultancy, and was asked in during the interview if I wasn't overqualified. The week I got my first paycheck I went down to the office and dropped out.

2024-07-13 07:25:40 UTC

the purpose of a system is what it does and what war thunder does is convince nerds to leak military intelligence when they're malding

2024-05-10 20:48:53 UTC

Love walking half way down the terminal 2 buy a can of coke for thrice its normal price

2023-06-28 14:26:37 UTC

boost this cat with nontrivial delay
https://pool.jortage.com/typespl/media_attachments/files/110/622/300/122/048/315/original/9588d72a5fc53f18.jpg