a language for talking about math precisely

[gusl]

I 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".

Comments

[gustavolacerda.livejournal.com]

Is my goal to replace traditional notation?

Well, I am a proponent of "dynamic syntax": one should be able to choose between traditional view (for scanners) and a more explicit view (for beginners)... or an integrated view, such as a tooltip telling you the type of the object whose identifier your mouse is on.

Of course, this is generally more work for content authors, at least until the system is intelligent enough to translate between the two automatically.

Ambiguity and terseness are also my main complaints with traditional notation.

PositiveDefiniteMatrix is definitely the kind of thing I have in mind.

I suspect that many difficulties will have to do with context-dependency.

Scanning is a concern I hadn't considered.