💾 Archived View for rosenzweig.io › gemlog › 2020-11-11-gemini-day-12.gmi captured on 2020-11-12 at 04:49:17. Gemini links have been rewritten to link to archived content
-=-=-=-=-=-=-
Nope. I promise, I'm trying to get a proper gemlog out, but the words aren't coming unless I force them and if I do that (as I am doing now), you'll end up with stream of consciousness about the fact that I'm struggling to get words out about Geminispace. I just, I don't do well with changes to my routine, okay? It's not my fault, it's Alyssa's fault. (...Ah, shoot.)
I wrote a dizzying amount of LaTeX at work today. Progress is slow on the Bifrost scheduler, but I'm starting to feel comfortable with the problem space, which is more than I could have said a few days ago. I think I've finally finished specifying the program model and all the invariants required, as well as proofs that the invariants really suffice to induce architecturally valid code; a proof is more powerful than a haphazard assertion. With a dozen pages of yak shaving out of the way, I can specify the algorithm in terms of the model and the model invariants, both of which are substantially simpler than the actual immediate representation and the architectural constraints, which will simplify both the construction of the scheduling algorithm as well as the proof of correctness.
The bad news is that even with simplification, there are pages of invariants required. Since the algorithm will be iterative, it looks like the algorithm proof of correctness can be expressed naturally as a proof by induction. Unfortunately, that means the induction hypothesis alone takes pages to write out in full.
Fun times lay ahead.
---
The usual disclaimers about my Internet use apply from yesterday. I have not regressed since then; I am still on a zero B.S. digital diet, and I am nearing the two week mark. I am noticing my drive to scroll through that sort of junk content has all but disappeared. Indeed, I am no longer forcing myself not to navigate to a problematic website; the urge just isn't there with a clearer head. Efforts to manage email, texting (Signal), and instant messaging are paused for the time being; as stated, I don't like change, and there is enough change throughout my life right now that adding a computing paradigm shift into the mix is inappropriate.
A recurring issue is the use of Signal, which sits snugly in the category of belonging to the big Internet and suffering from some serious flaws as such, while being nominally free software. I continue to use Signal out of lack of options. It is better than PSTN/SMS -- or at least, no worse -- and it is the only free software voice-over-IP application I have found that I can expect non-technical people in my life to setup for themselves.
Don't get me wrong; I would love to replace Signal with something "properly" free software, with XMPP and Matrix the best contenders. Unfortunately my experiences with both, particularly for telephony, have been suboptimal, and overall not something I can recommend in good faith to (for example) non-technical older family members.
However, for a long time Signal's telephony only worked on their Android/iOS clients. Nowadays there is support on their desktop client, but they do not provide builds of the desktop client for non-x86 architectures, and the application is not available in distribution repositories. Building from source for arm64 is a tortuous affair, fraught with ugly hacks, and the effort there is being lead by a single community member with no support (as I can see) from upstream.
I am not here to complain about platform support of any particular application; I understand the calculus involved, and I am well aware that preferring to only use arm64 Linux machines puts me in a tiny minority of a tiny minority. Still, the only computers I own are arm64/armhf Chromebooks, plus the Android phone.
The Android phone which has been moments away from breaking for the better part of six months now, and whose condition only continues to deteriorate. The battery seems to be the primary failing part, and the type-C port appears to have some degree of physical damage, although it's an entirely possible an embedded controller issue is masquerading symptoms of the above. Anyway, I don't want a phone, and theoretically do not need a phone. I do SMS/PSTN over XMPP/SIP respectively thanks to jmp.chat, a free software service I am more than happy to recommend. (Not affiliated, just a happy customer.) I use my GNU/Linux machines for all general-purpose computing. In effect, the phone is a dedicated Signal device now. That bothers me.
I do have options. I can fight for hours trying to get Signal Desktop running on one of the laptops (and even then I'm not sure I trust it on the same machine as anything of substance). Or, I can purchase an Android device or an x86_64 device. None of these are good options; a shortage of working hardware is not the issue here. Running the Signal client in Anbox is prohibitively slow and does not work for telephony due to missing microphone support in Anbox.
Oh, for completeness, I could port Android to one of the spare Chromebooks. Ha.
I said I had options.
I never said I had _good_ options.