[geckones]

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