spectrum of formalized scientific documentation

This post is an expansion of July 2020 post which was informed by Kaliszyk's survey.

Spectrum of formality:

category	verbal natural language	verbal presentation with aids	written text	semantic enrichment	human-oriented controlled natural languages	machine-oriented controlled natural languages	computer algebra systems	proof assistants, theorem provers
media	human speaking	human speaking; Latex containing text and equations -- Beamer	Latex containing text and equations and hyperlinks	Latex containing text and equations and hyperlinks; sTex	AIDA, ACE	text: RDF, OWL mathematical physics: Physics Derivation Graph math: ForTheL, Mizar	SymPy	Coq, Lean, Isabelle
purpose	social knowledge transfer, one-to-one	social knowledge transfer, one-to-many	human readers; text search	human readers; semantic search	consistency validation of logical claims	inference of novel knowledge	correctness of inference rules; dimensional consistency; unit consistency	mathematical correctness (consistency wrt a logical basis)
grouping	standard practice			knowledge representation			mathematical correctness
techniques				manual annotation; supervised machine learning	needs vocabulary and grammar: Mizar vocab ForTheL grammar PDG grammar

Left side of the spectrum is less rigorous, right side is more rigorous. 

Left side of the spectrum has higher de Bruijn factor, right side has lower de Bruijn factor.

The Physics Derivation Graph is a machine-oriented controlled natural language that is integrated with a computer algebra system.

Semantic tagging can relate definitions for terms within a document to the associated variables used in that document. 
The motive for the semantic tagging is to enhance search-ability. Since search-ability doesn't benefit the author, the author is not motivated to do the work of tagging.

Semantic tagging can identify common words across documents in a corpus. OWL is interesting conceptually but since the author doesn't benefit, the author is not motivated to do the work of linking.