All posts by Makarius

Bitcoin, das Zahlungsmittel der Zukunft? Was ist dran am Bitcoin-Hype?

Die Internationale Kelleruni Herrenbach veranstaltet im April eine öffentliche Vorlesung über Bitcoin und Blockchain.

Thema:
Bitcoin, das Zahlungsmittel der Zukunft? Was ist dran am Bitcoin-Hype?
Referenten:
Dr. Makarius Wenzel
Autor Christoph Ulrich Mayer
Zeit:
Freitag, 13. April 2018 um 19:30
Ort:
Lebensraum Schwabencenter (“Wohnzimmer”)

Das “Wohnzimmer” im Schwabencenter ist ein umgenutztes Ladenlokal innerhalb des regulären Einkaufszentrums. Nach der Vorlesung gibt es noch etwas zu Essen.

Peter Biet von der Kelleruni schreibt hierzu:

Ich selber bin auf diese Vorlesung sehr gespannt, denn ich lese davon ständig in der Zeitung. Ich höre von vielen gerade jungen Menschen, die relativ große Summen in Bitcoins investieren und damit dann auch tatsächlich “richtig Kohle” machen. Ich höre von der Möglichkeit, Geldflüsse unabhängig von Banken zu inszenieren, aber auch von Schwarzgeldern, die da gewaschen werden. Ich höre außerdem von den riesigen Rechnerleistungen, die benötigt werden, um Bitcoins zu schürfen. Und vor allem weiß ich Eines: Ich verstehe das Ganze überhaupt nicht. Finde, obwohl ich versucht habe, mich zu informieren einfach keinen Zugang zu der Sache.
Vielleicht geht es manchen von euch ja genau so. Jedenfalls bin ich des Öfteren gebeten worden, dass wir uns mal dieses so aktuellen Themas annehmen sollten. Und so freue ich mich sehr und bin gewiss, dass Makarius und Christoph da etwas Licht in mein/unser Wissensdunkel bringen werden.

Hier das Material von Makarius.

Further Scaling of Isabelle Technology

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

  1. Editing: Prover IDE,
  2. Building: batch-mode tools and background services,
  3. Browsing: HTML views and client-server applications.

Scaling Isabelle Proof Document Processing

Isabelle applications (e.g. from AFP) are growing steadily in size and number. To outline requirements and possibilities of the technology, I have produced a document on Scaling Isabelle Proof Document Processing.

Abstract:

This is a study of performance requirements, technological side-conditions, and possibilities for scaling of formal proof document processing in Isabelle and The Archive of Formal Proofs (AFP). The approaches range from simple changes of system parameters and basic system programming with standard APIs to more ambitious reforms of Isabelle and the underlying Poly/ML system. The running examples for typical scalability issues are existing formalizations of classical analysis and differential equations. Such applications can be further extrapolated towards a development of Financial Mathematics (e.g. Itô calculus).

Future Prospects of Isabelle Technology

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

Isabelle/VSCode 1.0 in Isabelle2017

The new Isabelle2017 release includes support for VSCode as alternative Prover IDE front-end. This continues earlier experiments and is released as Isabelle/VSCode 1.0. Note that Isabelle/jEdit had its 1.0 release in October 2011 and is presently at version 9.0.

Isabelle2017 provides the main Isabelle/Scala/PIDE functionality to connect to VSCode, using the official Language Server Protocol (with some PIDE add-ons). The front-end requires the extension called “Isabelle2017” from the VSCode marketplace: its README provides more information and installation instructions.

The Isabelle/VSCode project has been made possible thanks to funding by Aesthetic Integration (Grant Passmore and Denis Ignatovich).

Isabelle Docker image

The new Isabelle2017 distribution provides a Docker image via the Docker Hub repository.

The Docker image contains Ubuntu Linux with Isabelle2017. It can be used, e.g. on another Linux host like this:

  • docker pull makarius/isabelle:Isabelle2017
  • docker run makarius/isabelle:Isabelle2017

That provides command-line access to the regular isabelle tool wrapper, with indirection through the Docker container infrastructure.

The image already contains ML heaps for Isabelle/Pure and Isabelle/HOL. Here is an example to build more:

  • docker run makarius/isabelle:Isabelle2017 -s -b HOL-Library

Note that Docker is mainly for command-line tools on the “Cloud”. There is presently no Isabelle Prover IDE support, although very old-fashioned X11 connections can be made to work with extra tinkering.

Release candidates for Isabelle2017

We are heading towards the Isabelle2017 release, which is scheduled for October 2017. This spot provides a reference for upcoming release candidates.

  • Isabelle2017-RC0 (15-Aug-2017): informal snapshot for early experimentation. See also AFP/c98eb24b3598.
  • Isabelle2017-RC1 (03-Sep-2017): first official release candidate; almost everything ready, but some documentation still needs update. See also AFP/c7574e891704.
  • Isabelle2017-RC2 (08-Sep-2017):
    • improved Nunchaku model finder: now in Main HOL;
    • more HOL-Analysis material;
    • clarified dependencies of theory HOL-Library.Monad_Syntax;
    • robustification and fine tuning of Isabelle/jEdit.

    See also AFP/dfb6f8bc70e3.

  • Isabelle2017-RC3 (23-Sep-2017):
    • Isabelle/VSCode: improved treatment of Unicode vs. Isabelle symbols.
    • Documentation for “isabelle imports” in system manual.
    • Update of Isabelle/jEdit documentation.
    • Update of E prover and CVC4 for 32bit platforms.
    • Fine-tuning and polishing.

    See also AFP/dcf4dc3a3594.

As usual, the Isabelle release process is subject to the laws of causality: release candidates can be modified, but the final release is unchangeable. This means that testing needs to happen in the weeks before the final release, not after it.

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

Update 09-Oct-2017: The final release of Isabelle2017 (October 2017) is now available from the Isabelle website. The above release candidates will disappear eventually.

The Isabelle Prover IDE after 9 years of development, and beyond

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:

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.