All posts by Makarius

Social Networks in the Isabelle and Coq community

Here is an interesting (draft) paper about Social Network structures in the Isabelle and Coq community, based on the main mailing lists of the two systems:

J. Fleuriot, S. Obua, Ph. Scott: Social Network Processes in the Isabelle and Coq Theorem Proving Communities. arXiv:1609.07127, September 2016.

Just a few comments of mine:

  • The isabelle-users mailing list is still the main forum for Isabelle users, but Stackoverflow is gaining more and more importance. Note that I helped to bring it in form in Mar-2013 (earning a badge for 30 days of continuous activity :-), but I am rarely participating there now, because I am too busy with the classic mailing lists.
  • The seasonal peaks on isabelle-users in Fig. 1 are due to the release process, which happens approx. every 8-10 months. In 2012, I started to make discussion of release candidates fully public on isabelle-users; before it was confined to isabelle-dev, which is also open to everyone, but has fewer participants.
  • Page 12: “This seems to indicate that there is some clear separation of expertise when it comes to the tool.” This is correct and follows a general principle of Isabelle development: there are areas of undisputed “experts” for certain parts of the system. Thus there is a clear responsibility to make that thrive in the long term. Often this assignment is a consequence of starting that area in the first place, or investing significant work in upgrading it (e.g. by a designated PhD or research project). My recurring appearance on Sledgehammer threads is mainly technological: I am responsible for underlying infrastructure for parallel ML programming and the Prover IDE; it also overlaps with overall system integration and release management due to the add-on ATP and SMT systems.
  • In recent years, I have economized my appearance on isabelle-users as follows:
    1. Incoming messages are marked as important, when the topic overlaps with my areas of expertise. I rarely answer on the spot.
    2. After some days, weeks, or months, I revisit marked message and make sure that questions are actually answered, or add a few remarks to discussion threads.
    3. During the release candidate phases, I revisit all marked messages back to the previous release (or even one before that), to make sure that old technical problems are solved or remain in a reasonably well-defined state.

    This means the mailing list also serves as an “issue tracker”. I’ve made some experiments with an explicit tracker just for the release process, but there was very little participation. Trackers tend to become a long-term storage for well-known and unresolved problems.

Flattr this!

Visual Studio Code as Prover IDE for Isabelle

Microsoft is more and more becoming an Open Source company, e.g. it has joined the Linux foundation as Platinum member in November 2016. A notable Open Source project by Microsoft is Visual Studio Code: under the slogans “Code editing. Redefined. Free. Open Source. Runs everywhere.” it provides a very interesting editor framework, as a desktop application based on Node.js and TypeScript.

The prover community has already started to support this emerging successor of vi and Emacs, e.g. see Coq Support for Visual Studio Code and the Lean for VSCode.

Isabelle/VSCode is now following this trend: I have spent some weeks in December 2016 / January 2017 with VSCode, using a little bit of TypeScript and implementing the new Language Server Protocol in Isabelle/Scala. The subsequent screenshot shows formal annotations produced by Isabelle/PIDE in the usual manner, while the editor rendering is all done by VSCode. For more information, see the report Isabelle/VSCode in January 2017.

The Isabelle/VSCode project was funded by Aesthetic Integration (AI). See also my article about a talk at ITP 2016 by Grant Passmore (co-founder of AI).

Flattr this!

Provider change for sketis.net

After almost 12 years I have now changed the provider for sketis.net. This is the first post on the new platform, as a constructive proof that it really works!

Moving a classic toplevel domain (like .net) requires extra care and extra time. For almost 2 weeks nothing happened. Then there was a mail indicating failure of the procedure. After restarting the process it worked out surprisingly fast, within only 1 day instead of 5 days specified in the official mail text.

Now it might require additional 48h until the last corner of the Internet has noticed the new address of http://sketis.net.

Flattr this!

Foundations of Higher-Order Logic at Curry Club Augsburg

On Thu 01-Dec-2016 there will be a presentation about “Foundations of Higher-Order Logic with Classical Reasoning and Hilbert-Choice” at Curry Club Augsburg.

Start: approximately 19:00
Duration: approximately 90min
Language of the talk: German

Overview:

  • History of Higher-Order Logic
  • Implementations of HOL
  • Quasi-programming in Isabelle/HOL
  • Isabelle foundations: primitive inferences, object-logic rules, rule composition, structured proofs
  • Foundations of Higher-Order Logic: actual Isabelle/HOL, Pure bootstrap of HOL
  • Isabelle theory with some exercises (for Isabelle2016-1)

Flattr this!

Release candidates for Isabelle2016-1

The coming Isabelle2016-1 release is scheduled for December 2016. This spot is continuously updated to inform about the ongoing process of testing release candidates.

  • On 07-Oct-2016 an informal snapshot Isabelle2016-1-RC0 was published.
  • On 28-Oct-2016 the release candidate Isabelle2016-1-RC1 was published. Serious testing by users is now required, to expose remaining problems.
  • On 06-Nov-2016 the release candidate Isabelle2016-1-RC2 was published. Various details have been consolidated.
  • On 22-Nov-2016 the release candidate Isabelle2016-1-RC3 was published. More fine points have been consolidated. A component for the new experimental Nunchaku tool has been included.
  • On 27-Nov-2016 the release candidate Isabelle2016-1-RC4 was published. It introduces the following important last-minute changes:
    1. Prover IDE: more aggressive flushing of machine-generated input
    2. Sledgehammer: MaSh is faster and less likely to hang seemingly forever
    3. fine-tuning of Isabelle/LaTeX typesetting
  • On 08-Dec-2016 the release candidate Isabelle2016-1-RC5 was published, presumably the last one. It introduces the following important last-minute changes:
    1. more uniform automatic indentation (empty vs. non-empty lines)
    2. fewer tracing/warning messages in some proof tools

The Isabelle release process is subject to the laws of causality: release candidates can be modified, but the final release remains final. Testing needs to happen in the weeks before the final release, not after it.

The main forum for discussion of Isabelle2016-1 release candidates is on isabelle-users mailing list.

Update 13-Dec-2016: The final release of Isabelle2016-1 (December 2016) is now available from the Isabelle website. The above release candidates will disappear eventually.

Flattr this!

Isabelle/PIDE as IDE for ML

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).

Flattr this!

Isabelle/PIDE — from Interactive Theorem Proving to Integrated Theorem Proving

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.

Flattr this!

Grant Olney Passmore on Formal Verification of Financial Algorithms

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):

  • Collateral Trading
  • Inventory Management
  • Algo Containers
  • Trading Algorithms
  • Smart Order Routers
  • Venues

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.

Flattr this!