Mastodawn

I think my code suffered from a kind of subtle version of the “Goodbye, Lenin” problem — which was hard to tell since I have never run it 🫠🤣

But yesterday I took some time to rearchitect things and I believe I have forestalled any possible version of this. Famous last words, etc., etc.

I’ve also (I believe!) corrected my implementation of observational postponement, which had been way too naïve and wasn’t stable under weakening.

Show thread

Jon Sterling 5d ago

Implementing proof assistants is really arcane, isn’t it? If I were reading this post as someone inexperienced in this area I would think it was gobbledygook.

Show thread

Morgan Arnold 4d ago

@jonmsterling can confirm! i've been trying to follow along with development, and it's damn hard to follow without a lot of rather specific background in the implementation of dependently typed programming languages. i've been trying to learn, but it's definitely not the easiest thing to break into

Show thread

Morgan Arnold 4d ago

@jonmsterling oh, out of curiosity, is continuing with the current implementation of pterodactyl written in swift the long-term plan for the language, or is the plan to write a proof-of-concept implementation in swift before pivoting to an implementation in some other language? i ask because i spent a bit of time yesterday attempting to build pterodactyl locally on my machine and ran into... issues. indeed, i'm not sure if it's possible to build pterodactyl on linux?

Show thread

Morgan Arnold

@jonmsterling i documented some of the specific issues that i ran into here: https://mathstodon.xyz/@mra/116286636195133945, but they probably aren't of much interest. there are a lot of nixos-specific issues that i ran into, but the crux of it seems to be that `.linux` is not a `SupportedPlatform`, so it can't be added to the `platforms` field of the `package` declaration in Package.swift.