I updated the tutorial and the game; the most prominent update is that the editor now suggests fixes that solve copy/paste and mechanical editing. It makes the experience a lot better.
I also refactored the tutorial to be more introductory about the project.
Yeah, I guess I can fix this easily by using qed instead of wip in the templates, but I have to check if the error messages will persist, I believe the qed error suppress the helpful messages now.
But this does not scale, there is a lot of copy and paste when the proofs require case analysis, I want to check if I can emit edit comands to the editor in a sane way to automate that copy and pasting.
Yeah the game was thought to be an extension of the tutorial and an educational/grinding environment for the theory and the language.
About interacting with text, in that case I think it is exactly the opposite. The purpose is to be a funny shell around a bunch of exercises that would fell tedious (for me, at last) without it. It is meant to be a roguelike dungeon crawler about proof theory, so yeah, it is expected the player to learn to write proofs.
To me there are still 2 big problems
1. The language ergonomics. This is what I want to work on next.
2. The progression of the game levels and the tutorial. The goal is that they introduce the tool (algae), introduce proof techniques (ex: to proof a conditional you assume the premise and prove the conclusion) with some progression, and provide a playground through the game
The project (algae) is a algebraic specification tool. This means it is intended to allow you to write algebraic specs, in which you define your data types (sorts), operations (ops), and the the equations chatacterizing the operations (axioms). It is a formal specification technique. I designed because I want something to pratice/improve my proof theory skills, so, distinct from Lean4 or Roqc, all the proof information is visible in the surface syntax, but it still lack ergonomics.
About the tutorial and the game, I want it to be "proof theory introction"-like but the generated proofs are really not as good as I want they to be. The dificult progressions does not exist, the help sometimes does not help, some lemmas provide the proof in their arguments. To fix that I will need to go proof by proof and fix the help manually and also work on the progression. The AI is terrible at generating the proofs (yes it was made with AI help but I have formal specs experience).
About the game, it may still be buggy, feel free to open issues at https://github.com/dhilst/algae/issues, and I will fix it. I want to provide a cool playground for ppl to learn proof theory and for me to pratice it too.
I also refactored the tutorial to be more introductory about the project.