I have attended the Malinca project Kickoff-Meeting from 01..03-Oct-2025, and delivered an invited talk about Human-readable Proof Documents and Embedded Sublanguages in Isabelle/Isar.

Abtract:

Isabelle/Pure was originally introduced by Paulson (1986/1989) as a Logical Framework to specify object-logics declaratively, based on Higher-order Natural Deduction. Isabelle/HOL emerged soon as main object-logic and Isabelle application, with many tools for specifications and proofs written in Isabelle/ML.

Isabelle/Isar was added by Wenzel (1999) as a structured language for Human-readable formal proof documents: it works with Isabelle/Pure and regular object-logics. The proof language has been reworked over the decades, with notable extensions in 2015/2016, including the Eisbach language for Isar Proof Methods. Already, from the beginning, Isar had been accompanied by the Isabelle Document language, to write mathematical texts with high-quality typesetting in LaTeX.

So today we may see Isabelle as an agglomeration of many languages for different purposes, all integrated into a single System Framework in Isabelle/Scala. That includes the Isabelle/PIDE Prover IDE with parallel and asynchronous processing of formal documents, and the Isabelle build system (with its distributed cluster manager). Thus we can carry the weight and gravity of large proof documents, as e.g. seen in the Archive of Formal Proofs (AFP).