Update readme

README.md

@@ -3,3 +3,11 @@
 Highschool math and zero programming background? Not a problem, the idea of this game is to be extremely approachable. This is a work in progress, so feel free to open an issue to leave feedback of any sort.
 
 Here looking for answers to any of the levels? You can look under `Game/Levels/`. Each statement has a proof that uses only the tools the game has taught so far.
+
+# Discussion
+
+This game is currently in its initial development phase, designed to be largely self-contained and accessible without requiring a programming or math background to navigate. Feedback about meeting that goal is welcome!
+
+While self-contained; in many ways, this game is targeted more at programmers than mathematicians. It doesn't use classical reasoning, sticking instead to constructive logic. The emphasis for most of the theorem proving is on writting proof terms — rather than using tactics. In fact, logic proof automation is such that the tactic **`tauto`** can solve any propositional logic theorem (Though possible, that's an NP-Complete problem).
+
+The main thrust of this game is to create puzzles that are fun to think through on your own. I can write a simple algorithm that solves every proper Sudoku. Yet, when I spend a train-ride scribbling numbers into boxes in my sudoku book, I never lament how much faster my phone's CPU could do the job.