![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslI just spent >1 hour brainstorming/designing a heavily-typed language to help me formalize the math behind basic statistics and linear algebra. The fun of seeing mathematical objects with types like A -> B -> C is to consider mathematical concepts that arise out of currying it, reversing arrows, etc., and visualizing possible analogies between different concepts.
To paraphrase someone, the programs would be written to be read by humans, and only occasionally by computers. In particular, I'm designing it to be tolerant of incomplete formalizations/implementations (since formalizing "common-sense math" is so much work). This means it won't always be able catch contradictions... but I'm hoping it could learn to, by interacting with the user (turning "programming by demonstration" into "math acquisition by demonstration").
Currently I'm not distinguishing definitions from theorems. They're both "Constraint".
To paraphrase someone, the programs would be written to be read by humans, and only occasionally by computers. In particular, I'm designing it to be tolerant of incomplete formalizations/implementations (since formalizing "common-sense math" is so much work). This means it won't always be able catch contradictions... but I'm hoping it could learn to, by interacting with the user (turning "programming by demonstration" into "math acquisition by demonstration").
Currently I'm not distinguishing definitions from theorems. They're both "Constraint".