The slides for my presentations at FLoC 2018 (Oxford) are now available via the official “smart slide” service:
This is my contribution to the F-IDE workshop (14-Jul-2018, Oxford, UK): Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents.
Abstract:
Isabelle/jEdit is the main application of the Prover IDE (PIDE) framework and the default user-interface of Isabelle, but it is not limited to theorem proving. This paper explores possibilities to use it as a general IDE for formal languages that are defined in user-space, and embedded into informal text documents. It covers overall document structure with auxiliary files and document antiquotations, formal text delimiters and markers for interpretation (via control symbols). The ultimate question behind this: How far can we stretch a plain text editor like jEdit in order to support semantic text processing, with support by the underlying PIDE framework?
See also the official slides.
On Monday 05-Feb-2018, I will give a presentation about Further Scaling of Isabelle Technology at VU Amsterdam, invited by Jasmin Christian Blanchette. See also the official seminar website.
Abstract:
Over 32 years, Isabelle has made a long way from a small experimental proof assistant to a versatile platform for proof document development and maintenance. There has always been a challenge to keep up with the natural growth of applications, notably the Archive of Formal Proofs (AFP).
- Can we scale this technology further, towards really big libraries of formalized mathematics?
- Can the underlying Scala/JVM and Poly/ML platforms cope with the demands?
- Can we eventually do 10 times more and better?
I will revisit these questions from the perspectives of
- Editing: Prover IDE,
- Building: batch-mode tools and background services,
- Browsing: HTML views and client-server applications.
On 23-Nov-2017, I will give a presentation about Future Prospects of Isabelle Technology at DTU (Danmarks Tekniske Universitet), Copenhagen – thanks to an invitation by Jørgen Villadsen. More information on the meeting is available on the website.
Abstract:
In the past 3 decades, Isabelle has made a long way from a modest LCF-style proof assistant (with copy-paste of proof scripts written in ML) to the current Isabelle/PIDE editor-environment (with its timeless and stateless processing of proof documents). In this presentation, I will try to extrapolate this into the future: How far can we scale proof documents and libraries, e.g. via moving Isabelle into the “cloud”? How can we reduce system resource requirements on the client side? How can we upgrade interactive edits produced by a single author, towards versioned changesets by multiple or distributed authors? What are suitable frameworks for the next generation of Isabelle document preparation? What can we make out of Isabelle/ML as ultra-clean environment for functional programming? Etc. etc.
Sources for the presentation: Copenhagen2017.tar.gz
On Mon 24-Jul-2017, I gave a presentation at the BigProof event in Cambridge. Title: The Isabelle Prover IDE (PIDE) after 9 years of development, and beyond. Abstract:
The main ideas around Isabelle/PIDE go back to summer 2008. This is an overview of what has been achieved in the past 9 years, with some prospects for the future. Where can we go from here as Isabelle community? (E.g. towards alternative front-ends like Visual Studio Code; remote prover sessions “in the cloud”; support for collaborative editing of large formal libraries.) Where can we go as greater ITP community (Lean, Coq, HOL family)?
Here are some notable VSCode projects that were briefly mentioned in the talk:
On Friday 18-Nov-2016 10:00, I will give a presentation about PIDE at Laboratoire de Recherche en Informatique, Orsay (Paris Sud).
Abstract:
Isabelle is usually positioned as environment for interactive and automated theorem proving, but its Prover IDE (PIDE) may be used for regular program development as well. Standard ML is particularly important here, since it is the bootstrap language of Isabelle/ML (i.e. SML with many add-ons) and Isabelle/Pure (i.e. the logical framework).
The ML IDE functionality of Isabelle + Poly/ML is manifold:
- Continuous feedback from static analysis and semantic evaluation is already available for years, e.g. Isabelle2014 (August 2014). It is a corollary of how PIDE interaction works, and of the integration of the Poly/ML compiler into that framework. Source files are statically checked and semantically evaluated while the user is editing. The annotated sources contain markup about inferred types, references to defining positions of items etc.
- Source-level debugging within the IDE is new in Poly/ML 5.6, which is bundled with Isabelle2016 (February 2016). The Prover IDE provides the Debugger dockable to connect to running ML threads, inspect the stack frame with local ML bindings, and evaluate ML expressions in a particular run-time context. See also here.
- IDE support for the Isabelle/Pure bootstrap process is new technology for the coming release of Isabelle2016-1 (December 2016). The ROOT.ML file acts like a quasi-theory in the context of theory ML_Bootstrap: this allows continuous checking of all loaded ML files. The theory file is presented with a modified header to import Pure from the running Isabelle instance.
It is also possible to modify standalone SML projects, to edit the sources freely in the ML IDE. For example, MetiTarski can participate after some trivial changes of its ROOT.ML file.
Overall, we move more and more to an integrated framework for development of formal-reasoning tools, but other applications are admissible as well.
The Slides are available, together with their sources (which are required for the live system demo).
On Tuesday 15-Nov-2016 14:00, I will give a presentation about PIDE at Laboratoire Spécification et Vérification, Cachan (Paris). See also the official announcement.
Abstract:
Interactive theorem proving was historically tied to the read-eval-print loop, with sequential and synchronous evaluation of prover commands given on the command-line. This user-interface technology was adequate when Robin Milner introduced his LCF proof assistant in the 1970s, but today it severely restricts the potential of multicore hardware and advanced IDE front-ends.
The Isabelle Prover IDE breaks this loop and retrofits the read-eval-print phases into an asynchronous model of document-oriented proof processing. Instead of feeding a sequence of commands into the prover process, the primary interface works via edits over immutable document versions. Execution is implicit and managed by the prover in a timeless and stateless manner, making adequate use of parallel hardware.
PIDE document content consists of the theory sources (with dependencies via theory imports), and auxiliary source files of arbitrary user-defined format: this allows to integrate other languages than Isabelle/Isar into the IDE. A notable application is the Isabelle/ML IDE, which can be also applied to the system itself, to support interactive bootstrapping of the Isabelle/Pure implementation.
Further tool integration works via “asynchronous print functions” that operate on already checked theory sources. Thus long-running or potentially non-terminating processes may provide spontaneous feedback while the user is editing. Applications range from traditional proof state output (which often consumes substantial run-time) to automated provers and dis-provers that report on existing proof document content (e.g. Sledgehammer, Nitpick, Quickcheck in Isabelle/HOL). It is also possible to integrate “query operations” via additional GUI panels with separate input and output (e.g. for manual Sledgehammer invocation or find-theorems).
Thus the Prover IDE orchestrates a suite of tools that help the user to write proofs. In particular, the classic distinction of ATP and ITP is overcome in this emerging paradigm of Integrated Theorem Proving.
The Slides are available.
On 25-Aug-2016, Grant Olney Passmore from Aesthetic Integration gave an invited talk at the ITP 2016 conference in Nancy, France. Here is the official announcement from the program:
Title: Formal Verification of Financial Algorithms, Progress and Prospects
Abstract:
Many deep issues plaguing today’s financial markets are symptoms of a fundamental problem: The complexity of algorithms underlying modern finance has significantly outpaced the power of traditional tools used to design and regulate them. At Aesthetic Integration, we’ve pioneered the use of formal verification for analysing the safety and fairness of financial algorithms. With a focus on financial infrastructure (e.g., the matching logics of exchanges and dark pools), we’ll describe the landscape, and illustrate our Imandra formal verification system on a number of real-world examples. We’ll sketch many open problems and future directions along the way.
The session chair introduced the speaker as a colleague from the prover community who managed to get his private life covered by the NY Times.
Passmore then started his presentation with a promotional video, which is intended for people from the Financial Industry – without a background in formal logic or software verification. He pointed out that this is his first talk about the subject before an audience with expertise in theorem proving, and promised that many odd terms and buzzwords from the world of Finance would become clear later.
From his many slides, Passmore could fit only a small portion into the 60min time slot. A key point was the following Stack of Financial Algorithms (from top to bottom):
So far, Aesthetic Integration has mainly worked at the bottom: “Venues” are virtual places where trading happens, e.g. a “dark pool” as in the UBS Future of Finance Challenge (see also the white paper).
Passmore invited the prover community to participate in formal treatment of the whole stack given above. For example, full formalization of Financial Mathematics in Isabelle/HOL could support the slot “Trading Algorithms”.
He also presented the present flagship tool environment: Imandra. Here is a quotation from the official website:
What is Imandra?
AI’s Imandra is breakthrough artificial intelligence technology for ensuring financial algorithms are designed and implemented safely and fairly.
Powered by major recent advances in formal verification, Imandra:
- Verifies correctness and stability of system designs for regulatory compliance
- Uncovers nontrivial bugs
- Tests – creates high-coverage test-suites
- Saves – radically reduces associated costs
The system was demonstrated in two versions: one running on the local machine, and one running on a server (i.e. “in the cloud”). The interaction model is still mainly command-line based, but Aesthetics Integration is interested to improve on that.
At the Isabelle Workshop 2016 in Nancy, I presented a paper about recent renovations of the Isar proof language:
This is a description of the Isar proof language as it stands today in 2016. This means the official release Isabelle2016 (February 2016), and the next release that is presumably published towards the end of the year. Relevant NEWS entries and updated portions from the Isabelle/Isar Reference Manual are summarized in one comprehensive article.
The forthcoming release of Isabelle2016 provides substantial refinements of the Isar proof language, after many years. This is a consequence of clarification of Isar internals, in order to support the Eisbach proof method language (by Dan Matichuk et al).
These Slides provide an overview for Isabelle users who know classic Isabelle/Isar already.