I find that writing and mathematics are just a poor way of trying to structure a context free domain specific language for the problem.
Writing is bad because it needs to fit in a human head and ultimately needs to be spoken by a human mouth. Maths is bad because it is still stuck as being written on blackboards or pen and paper if you're unlucky.
The few times I have build up these dsls formally have let me understand a topic both more deeply and remember it more easily. The downside is that time invested in inventing it in the first place. E.g.
(for-all x (implies
(member x integers)
(exist-unique y
(and (member y integers)
(equal? 0 (+ x y))))))
Is the way to say that all integers have additive inverses. It's ridiculously long but logically sound and quite easy to prove mechanically given that every operator in that sentence also have definitions in that vain.
Writing is bad because it needs to fit in a human head and ultimately needs to be spoken by a human mouth. Maths is bad because it is still stuck as being written on blackboards or pen and paper if you're unlucky.
The few times I have build up these dsls formally have let me understand a topic both more deeply and remember it more easily. The downside is that time invested in inventing it in the first place. E.g.
Is the way to say that all integers have additive inverses. It's ridiculously long but logically sound and quite easy to prove mechanically given that every operator in that sentence also have definitions in that vain.