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.

@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

@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?

@mra I expect to stay with Swift. It should indeed be possible to build with Linux, but I haven't tried. Swift is used on Linux all the time, and I'm certain there is no obstacle to building via Package.swift (but maybe I need to change it in some way)...

@jonmsterling ah, you're right that it is possible to build on linux. i guess i misunderstood the meaning of the `platforms` field. my issue appears to be a nixpkgs issue, since the status of swift support in nixpkgs is pretty abysmal. the best i can do is to compile pterodactyl within one of the docker containers provided by the swift folks. this works, but i can't run the resulting binary on my system because it's dynamically linked, and i can't patch it because the required libraries aren't in nixpkgs