ok I guess this could theoretically make sense if all access went through some privileged daemon, then you basically have a microkernel architecture

allwinner did not do that

like what is even the point of kernel drivers then. just have all applications open /dev/mem and go wild

wow allwinner's "official driver" really just mmap'd the hardware into userspace huh

the thing can DMA to whatever address you give it....

maybe my real contribution will be making voice/video rooms actually work without needing to be full mesh (and without needing to run webshit)

probably not anytime actually soon.

but I will read obsessively about how the protocol works, how webrtc, ice, rtp, etc. work, and what interfaces I'd need to use to get gstreamer to encode/decode webrtc, and hook that into a gtk application (answer: all the hard parts are done, and have gobject bindings, so I can get bindings in haskell or some other nice language)

I guess, your constructive definition of a != b might contain some information that's needed to construct an inverse. E.g. for power series, it could tell you the first coefficient for which a and b differ, which you'd need to know to constructively define 1/(a-b).

Ok so apparently one way to solve this is to have an *inequality* relation that explicitly comes with your structure. Then you can make the condition "if a != 0, then a is a unit". And I guess inequality might have a more subtle definition than just the negation of equality...

saying something like "assuming LEM, the real numbers are a field" just sounds fucking comical to me

ok so I think my next procrastination sink will be trying to formalize random bits algebraic geometry in HoTT using agda

first time to read a bunch of shit about how algebra even works constructively. like how do I even define "field". if it's like, "all elements are either 0 or invertible", then the real numbers aren't a field, because checking if a number is 0 isn't decidable????

I do not understand univalence in the slightest but apparently it means I can stop giving a fuck if things are "only isomorphic" and treat them like they're equal? That sounds cool and is basically how everyone already thinks about math I guess

Ok so I just learned these things are called "capabilities" and lots of systems like this exist, some modern and some from like 1970.

I want to make one...

dark mathemagician | 24 | they/them or she/her

I spent a lot of time on algebraic geometry. Now I spend a lot of time on computers.

Joined Jun 2020