Live data from Hacker News

Dungeon Proof Crawler: learn how to write proofs with RPG

dhilst.github.io

21–28 of 28 posts

Re: Dungeon Proof Crawler: learn how to write proofs with RPG

#21
post #17

The developer here! Thanks for all the feedbacks, here are some more info There is a tutorial: https://dhilst.github.io/algae 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 designe…

To me, what makes a game a game is that you can learn how it works simply by interacting with it; you don't need to open a separate wiki. That is not entirely true, as for examples fighting games have been infamous for needing to go online to learn how combos work, but this is widely considered to be a major factor of why the genre is unpopular, and recent games have tried to at least give proper tools (in training m…

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

Re: Dungeon Proof Crawler: learn how to write proofs with RPG

#22

The developer here! Thanks for all the feedbacks, here are some more info There is a tutorial: https://dhilst.github.io/algae 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 designe…

Have you looked at Metamath Zero[1] before? You mentioned using sorts which is what reminded me of it. Just thought I'd point to some additional interesting work :) [1] https://github.com/digama0/mm0

I didn't thanks for sharing

It looks a cool project, definetely related

Re: Dungeon Proof Crawler: learn how to write proofs with RPG

#23

Having to replace wip with qed when indentation makes it clear it's the only thing that fits is a bit tedious.

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.

Re: Dungeon Proof Crawler: learn how to write proofs with RPG

#24

Having to replace wip with qed when indentation makes it clear it's the only thing that fits is a bit tedious.

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.

Wouldn't it be better to improve the proof language so that copy-pasting is not necessary? (I know that's very hard, though.)

Re: Dungeon Proof Crawler: learn how to write proofs with RPG

#25

The first and southwest-most sphinxes of seed 0 never load, which soft-locks the game. (Fortunately it doesn't corrupt the save-file.) Edit: after fighting enough other sphinxes, the first one loads, but the west-most fails with an explicit error message: > This challenge failed to load. Retreating. On the next floor, the sphinx over the exit stairs fails, preventing me from progressing.

Oh you just said "seed 0" I will try it

[dead]

Re: Dungeon Proof Crawler: learn how to write proofs with RPG

#27

Earlier quoted context omitted.

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.

Wouldn't it be better to improve the proof language so that copy-pasting is not necessary? (I know that's very hard, though.)

I improved the editor to allow auto-completion, and clicking on the errors almost always suggests a fix. wip -> qed always work. (:
Post reply on HN