Heh, still in the early days of this! Let me know if you have any questions!
Is it still under development?
Yup! Actively working on it on the next branch, which is linked on this story. Hoping to merge it into the main branch, but having fun with second-system syndrome. It’s not super ready for public consumption yet, unless you want to get stuck into type system/compiler implementation with me! Haha!
Not to be confused with the Pike programming language: https://pike.lysator.liu.se/
Pike is based on LPC, which you might have used if you were a creator / wizard / admin on an LPmud. I believe there’s some kind of continuity in development too; the lysator.liu.se domain hosted a lot of MUD content.
Wow, that takes me back! Roxen AB, one of the backers of Pike, is named after the lake and apparently pike can be fished there.
What is the most advanced proof that has been done using Pikelet? It would be useful to see comparisons of proofs in Coq, Agda, Idris and Pikelet.
Is there a hierarchy of universes? I believe that is still missing in Idris. Is that necessary for Pikelet to be sound?