1. 20

  2. 8

    Heh, still in the early days of this! Let me know if you have any questions!

    1. 1

      Is it still under development?

      1. 1

        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!

    2. 2

      Not to be confused with the Pike programming language: https://pike.lysator.liu.se/

      1. 4

        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.

        1. 2

          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.

        2. 2

          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?