> > > Thirdly I recently came across literate programming > <https://en.wikipedia.org/wiki/Literate_programming> for the first time. > I think it's a really interesting idea and immediately made me think of > metamath. If it were possible to write proofs in natural language and then > have macros replace the natural language with mm steps I think that could > be a really powerful way of bridging the gap between beginners and > experienced users. >
Honestly if you think that you will be able to use a system of formal logic withouth spending a decent amount of time on it, without learning logic and set theory and without breaking your head, stop right now. Literate programming is not about replacing computer languages by natural languages. It is about reversing the relative importance of comments and code. Comments become more important than code. It's about writing an essay and then adding code. This way the problem is better understood and the code is of better quality. -- FL -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1ec7e8aa-2219-425a-8a49-fcf64dd511a1%40googlegroups.com.
