All posts by Makarius

Book available: “All about Proofs, Proofs for All”

As a result of the APPA workshop at Vienna Summer of Logic 2014, there is now a book available with the collected contributions by the invited experts (including myself). It is edited by Bruno Woltzenlogel Paleo and David Delahaye, and is published by College Publications. Here is a copy of the abstract from it:

The development of new and improved proof systems, proof formats and proof search methods is one of the most essential goals of Logic. But what is a proof? What makes a proof better than another? How can a proof be found efficiently? How can a proof be used? Logicians from different communities usually provide radically different answers to such questions. Their principles may be folklore within their own communities but are often unknown to outsiders.

This book provides a snapshot of the current state of the art in proof search and proof production as implemented in contemporary automated reasoning tools such as SAT-solvers, SMT-solvers, first-order and higher-order automated theorem provers and proof assistants. Furthermore, various trends in proof theory, such as the calculus of inductive constructions, deduction modulo, deep inference, foundational proof certificates and cut-elimination, are surveyed; and applications of formal proofs are illustrated in the areas of cryptography, verification and mathematical proof mining.

Experts in these topics were invited to present tutorials about proofs during the Vienna Summer of Logic and the chapters in this book reflect their tutorials. Therefore, each chapter is intended to be accessible not only to experts but also to novice researchers from all fields of Logic.

My contribution to the book is a chapter on “Interactive Theorem Proving — from the perspective of Isabelle/Isar”, with the following abstract:

Interactive Theorem Proving (ITP) has a long tradition, going back to the 1970s when interaction was introduced as a concept in computing. The main provers in use today can be traced back over 20–30 years of development. As common traits there are usually strong logical systems at the bottom, with many layers of add-on tools around the logical core, and big applications of formalized mathematics or formal methods. There is a general attitude towards flexibility and open-endedness in the combination of logical tools: typical interactive provers use automated provers and disprovers routinely in their portfolio.

The subsequent exposition of ITP takes Isabelle/Isar as the focal point to explain concepts of the greater “LCF family”, which includes Coq and various HOL systems. Isabelle itself shares much of the relatively simple logical foundations of HOL, but follows Coq in the ambition to deliver a sophisticated system to end-users, without requiring self-assembly of individual parts. Isabelle today is probably the most advanced proof assistant concerning its architecture and extra-logical infrastructure.

The Isar aspect of Isabelle refers first to the structured language for human-readable and machine-checkable proof documents, but also to the Isabelle architecture that emerged around the logical framework in the past 10 years. Thus Isabelle/Isar provides extra structural integrity beyond the core logical framework, with native support for parallel proof processing and asynchronous interaction in its Prover IDE (PIDE).

Flattr this!

Proposal: remote prover connectivity for Isabelle/PIDE

(See also general notes on proposals.)

“Cloud computing” is one of these buzzwords without any particular meaning, but the idea to run heavy-duty computations remotely is rather old: some “big-iron” in the background provides the CPU and memory resources for substantial applications, while the user interacts with the system via some small local terminal. Already in the classic days of Proof General (around 1999) it was common-place to run Emacs locally on a workstation and the prover process remotely on a server (via rsh). Alternatively it was possible to run both the editor and the prover remotely and use X11 as display protocol, which was especially important for the rather heavy XEmacs of that time.

This normal mode of distributed computing was almost forgotten, when the performance of local laptops and remote servers were approaching the same order of magnitude (due to the demands of the gaming industry). This was only an episode over a single decade, though, and we are already back to the traditional situation where local and remote machines can differ significantly. In 2014, typical mobile devices were limited to 2–8 CPU cores and 2–8 GB RAM. This is very little compared to low-end workstations or high-end servers, with something like 8–36 CPU cores and 32–512 GB RAM, or more.

Note that some big Isabelle applications already go beyond the possibilities of small machines with only 4–8 GB RAM, but for more memory Poly/ML process needs to be switched from 32-bit to 64-bit mode, which also doubles the memory demands. Thus there is a discontinuity here: stepping out of the “small device” category means to go for 16–32 GB RAM minimum.

This motivates the demand for remote prover connectivity for Isabelle and its Prover IDE (PIDE). The most basic approach is to run the internal socket connection for the PIDE protocol between ML and Scala over ssh. This should be sufficient for fast and reliable local networks. For non-local networks, there are the usual questions about bandwidth, latency, and reliability of the connection. The PIDE protocol requires relatively high bandwidth (which is easily provided by common DSL connections), but can afford high latency due to its asynchronous nature. Lack of reliability might turn out a real problem, though: resetting a lost TCP/IP connection naively means to restart the prover process and recheck the whole session from start, which could take minutes or hours.

Thus a more advanced approach would keep both the ML and Scala side of PIDE together on the server. Remote access then works via a separate PIDE display protocol, which is postulated here and still needs to be defined and implemented. Depending on active buffers and open text areas in the editor, the remote side would provide continuous access to incoming PIDE document markup, without demanding persistent management of the whole PIDE state locally. Loosing the connection would merely mean to reconnect the IDE to the remote Isabelle/Scala/ML component, which keeps running indefinitely.

Thus the mode of operation becomes more like the re-connection facility of VNC or RDP (but not X11). Of course it is already possible today with Isabelle2014 to use VNC or RDP for a completely remote ML/Scala/IDE process, but remote ML/Scala and local IDE would make this more comfortable for the user, with better graphics performance and reactivity.

Taking this perspective of remote PIDE sessions one step further could mean to support low-bandwidth, high-latency, unreliable connections of mobile networks: sitting on a train with a laptop and local IDE, while re-connecting to a remote PIDE session on a big server, would really count as cloud computing. We should think here of editing whole libraries like AFP on the spot, with immediate feedback. A bit more efforts will be required to get there, though.

In summary, the following stages are possible, depending on the amount of resources spent on this subject:

  1. Simple remote PIDE socket connection via ssh, usable for fast and reliable local networks. (The jEdit text editor already provides some means to manage ssh, so this merely requires the usual study of sources with subsequent tinkering and polishing to make it work smoothly.)
  2. Separate PIDE display protocol where the editor is local and the Isabelle/Scala/ML session is remote. This should be usable for fast DSL network connections.
  3. Support for smooth disconnection and re-connection for mobile networks.
  4. Development of a completely different PIDE front-end that works on tablets or smart-phones (Android or iOS).

The last point is speculative: it merely sketches to horizon of what could eventually be targeted, if there were lots of resources and several enthusiastic people working on it.

Flattr this!

General notes on proposals

This section of the website is meant to improve the Isabelle platform for Interactive Theorem Proving, as far as I am personally involved. Beyond that there are many users, contributors, and developers of Isabelle applications and add-on components world-wide, e.g. see the collected outcomes in the Archive of Formal Proofs as the visible universe of formally published results.

The category proposals collects articles on particular topics as they emerge over time. This may serve informative purposes on important lines of further Isabelle development, or as a starting point for discussion and elaboration — depending on specific demands of big and important applications out there.

Moreover, this is an explicit invitation to support proposals actively. A variety of ways are possible to do that:

  • Donate small amounts, potentially dedicated to a particular area of work that you want to see raised in priority. This may be understood as a modest form of crowdfunding.
  • Procure some funding as part of a bigger research or development project, and get me involved as an external contractor or consultant.
  • Invite me to your research or development group (at your expenses), in order to support you, your co-workers, your students, your users in advanced Isabelle applications. For example, the format could be an internal workshop of a few days, or a stay over a few weeks, to instruct prospective experts of Isabelle tool development.
  • More ambitious plans according to your particular requirements and possibilities.

I am ready to provide such professional services around the Isabelle platform that fit into my areas of expertise, and can be fulfilled with the side-condition of myself being mainly located at the center of Europe: Bavaria / Swabia / Augsburg. 2000 years ago that was the capital of the Roman province of Raetia. 500 years ago it was the commercial and financial center of the Western World (the Empire of Charles V), due to the Fugger family. Today it is my own base for research and development projects, where I am both remote and connected to the world.

Please contact me via email as given on the main page. Further local address details are given in the impressum (together with some formal German legalese).

Flattr this!

Coq/PIDE public beta

The first public beta of Coq/PIDE was released by Carst Tankink just a few days ago. See also the announcement on the coq-club mailing list from 26-Nov-2014.

Building it manually from individual parts was a bit tricky, but knowing in theory how things should fit together, I managed after two failed attempts. Note that COQBIN really needs an extra slash at the end, or the Makefile will break down.

Here is a screenshot of Coq/jEdit on Linux with GTK look-and-feel, editing a medium-sized file from the Coq library:

Coq-jEdit

There is an important conceptual difference to Isabelle/jEdit, which edits a whole project (or “session”) with many files active at the same time within the same prover process.

In contrast, Coq has capitalized separate compilation a long time ago, so it is likely that its one-to-one relation of files versus sessions (with a separate coqtop for each) will remain in years to come.

Update 02-Feb-2015: Carst Tankink has just announced the second public beta Coq/jEdit 0.2.0 for Coq 8.5beta1.

Flattr this!

Isabelle Tutorial at CADE-25

(See also updated version with more details.)

A full-day tutorial on Isabelle is scheduled as associated event of the 25th International Conference on Automated Deduction (CADE-25), which will take place in Berlin at the start of August 2015.

More than 25 years ago, Isabelle was initiated by Larry Paulson as a logical framework for rapid prototyping of Natural-Deduction proof systems. Today, Isabelle is one of the major platforms for Interactive Theorem Proving (ITP), with notable support for automated reasoning tools (ATPs and SMTs). Isabelle/HOL is the main environment for applications; it is accompanied by the Archive of Formal Proofs (AFP) as repository for user-contributions. Isabelle supports logical tool development in Isabelle/ML and Isabelle/Scala, but it is also possible to connect external tools; this works routinely on Linux, Windows, and Mac OS X. The system presents itself to the end-user by an advanced Prover IDE: Isabelle/jEdit.

The purpose of the tutorial is to help participants to get acquainted with Isabelle: topics will cover specifications in HOL, proofs in Isar, use of automated provers via Sledgehammer etc. The target audience are doctoral students or researchers with an interest in formalized reasoning, application of reasoning tools for interactive and automated proof development, maybe even with an interest to develop their own tools with/for Isabelle.

There will be presentations by myself and one or two colleagues, with hands-on tutoring and exercises done by the participants on their own computers (with at least 2 cores and 4 GB memory).

Further organizational details will emerge sooner or later, as summer 2015 approaches. Watch this space, as well as the main CADE-25 website.

Flattr this!

CICM 2015 at Washington DC

The Conferences on Intelligent Computer Mathematics (CICM) — with the distinctive sub-conferences Calculemus, DML, MKM — may be seen as a gathering of fringe groups, but a very interesting one. Traditionally, it may serve as a forum for experimentation and unorthodox contributions that are difficult to publish elsewhere.

I have served several times on the PC of Calculemus or MKM, and once as PC chair of MKM. For CICM 2015, I am PC member for Calculemus.

Don’t be confused by the website that is somewhat difficult to navigate! Don’t miss the start of the submission process: 16-Feb-2015 for abstracts, followed by actual papers, followed the  rebuttal phase. The latter is particularly important to readjust the initial verdict by the reviewers, going upwards or downwards, depending on careful reactions of the authors to what was said about their papers.

Flattr this!

Alexander Grothendieck

Born 28-Mar-1928 (Berlin, Germany), died 13-Nov-2014 (Saint-Lizier, France).

In my own studies, I have occasionally encountered the famous name of Grothendieck in lectures about functional analysis and logic. From a bit later, I remember discussions with Helmut Schwichtenberg about Tarski-Grothendieck set theory as the foundation of the formal mathematical language of Mizar.

In 2010, I came again across the name of Alexander Grothendieck several times, when searching the web about my new hometown Bures-sur-Yvette, where I lived until August 2014 only a few hundred meters from the famous IHÉS institute. That was the place where Grothendieck worked for some time at the peak of his mathematical life (until 1970). Afterwards he removed himself more and more from public and scientific life.

Winfried Scharlau has started to publish material about the life of Grothendieck some years ago, with this notable article from 2006/2008. There was also some activity on the web to collect more information, but this was stopped abruptly in 2010 with this angry letter from Grothendieck himself, speaking to the world from a secret place in the Pyrenees.

At least we now know that his last residence was in Lasserre (l’Ariège); see also this article of La Depeche.

Here is another blog with many more links.

Flattr this!

Isabelle/PIDE as IDE for Standard ML

Strictly speaking the Isabelle environment is for interactive and automated theorem proving, but its SML IDE support is quite sophisticated: 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.

As a quick start, see the Documentation panel, section Examples, entry src/Tools/SML/Examples.thy (as of Isabelle2014).

SML-PIDE

The time where SML sources need to be edited with vi or emacs are over. See also this related thread on Stackoverflow.

Flattr this!