#introductions
An introductions post, since I've got a bunch of new followers in the last couple of weeks (hello everybody!)
By day, I do computer verification of #math in the Lean prover, by night I do #osdev. When there isn't a plague going around, I like #cycling in nature and befriending #crows. I also know a bit of #linguistics.
I really like explaining concepts — feel free to ask any question (esp. mathematics / theoretical comp sci). Replies to toots are always welcome.
ME, ONE YEAR AGO: this mexican party is good, but it has... how can one say ... too many people? there are in fact, only so many people one can dance with in the course of a party. I think I'm right in saying that, aren't I?
MY WIFE: this is absurd!
ME: my dear, don't take it too hard. it's quality celebrating. there are simply too many people. just remove a few, and it will be perfect.
MY WIFE: which few did you have in mind?
the garbage collector goes through a whole collection cycle without causing kernel panics 🎉
(now I just have to fix the other processes crashing)
(or the usb driver's strategy of "ensure this buffer occupies a continuous section of virtual memory, by allocating a buffer the size of 2 memory pages and carving out a page-aligned section in the middle". for each send/receive operation. that could also be it.)
(one thing I should optimize soon: function arguments are currently passed as a linked list on the heap. can't test it yet, because the GC is broken, but that is probably the worst garbage generator.)
#osdev update: movement commands in the editor are starting to work, but my "write the simplest possible implementation, then come back to optimize it" approach is starting to cause out of memory within one (1) minute
so: time to (re)activate the garbage collector
so: time to actually debug the garbage collector now that garbage is being produced
so: time to crash, a lot
worse conlang idea: invent an international language where words are optimized to sound dirty to as many people as possible, then rename all theorem provers to words in this language
possessives are marked by a suffix /nə/, which triggers /u/ → /o/ and /i/ → /e/ ablaut in the root. 1.SG-POSS-ACC "my (accusative)" becomes /penəs/
@Vierkantor accusative forms are /pis/ and /pus/ then, of course
e.g. the 1st person singular pronoun is /pi/, 2.SG is /pu/, plurals are formed by reduplication, and inclusive "we" (I, you and them) is expressed as "we you" /pipi pupu/
/'ɑ.nə/ & legally certified as they who must become Master & (intuitionistic) maths / programming & pronouns: they/them (or best offer) & trains, crows and sheep & as seen in children's magazine