juleshPrediction: over the next decade or 2 the remaining basic principles of proof assistants will be figured out, and the first minimally viable language will be proudly handed over to the mathematicians, who will then look at the millions of lines of code they've already written in Lean and collectively decide to just keep building on that. Only another decade or 2 after that will they learn the meaning of "technical debt"
GNU social JP is a social network, courtesy of GNU social JP管理人. It runs on GNU social, version 2.0.2-dev, available under the GNU Affero General Public License.
All GNU social JP content and data are available under the Creative Commons Attribution 3.0 license.