Maybe I am weird, but I would like to see/program in a formal, yet fuzzy/modal language, which could serve as a metalanguage that describes (documents) the program. This metalanguage must have some kind of constructs to describe unknown things, or things that are deliberately simplified in favor of exposition. So basically eschew natural language completely in favor of fully formalized description, that could be manipulated programmatically.

However, I don't know what this metalanguage should be. I don't know how to translate typical comments (or a literate program) into some sort of formal language. I think we have a gap in philosophy (epistemology).

search for "Controlled natural language". Many attempts in the past - ~20y ago, one of these is even called "Attempto", near nothing recently. Seems not enough interest in wide audiences

> This metalanguage must have some kind of constructs to describe unknown things, or things that are deliberately simplified in favor of exposition.

Perhaps you're thinking of mathematics.

If you have to be able to represent arbitrary abstract logical constructs, I don't think you can formalized the whole language ahead of time. I think the best you can do is allow for ad-hoc formalization of notation while trying to keep any newly introduced notation reasonably consitent with previously introduced notation.