Email Gateway (Aug 22 2022 at 18:12): Email Gateway (Aug 22 2022 at 18:12):From: Talia Ringer <tringer@cs.washington.edu>
Hi all,
My name is Talia Ringer and I'm a Ph.D. student at the University of
Washington. I'm working on a proof engineering
<http://proofengineering.org/> survey paper. However, I don't have any
Isabelle expertise on the paper, and my community overwhelmingly skews
toward Coq users. To make sure Isabelle gets adequate coverage, I have been
consulting other people.
Right now, I am looking for noteworthy Isabelle proof developments to
include in the paper. The paper focuses mostly on proof engineering for
program verification, but it talks about mathematics and metatheory as
well, so developments in those domains are welcome. I'm aware of the AFP,
but please don't hesitate to link to particular developments within the AFP
if you think they're especially noteworthy. It is OK to send your own work
if you think it is noteworthy and want to make sure it isn't missed.
Also, while not the focus of this email, feel free to send other bits of
Isabelle knowledge besides major proof developments that you think are
essential to a survey paper (to give an idea of what sorts of things are
relevant, we already talk about Isar, the Isabelle style guide, Nominal
Isabelle, Transfer and Lifting, sledgehammer, and Isabelle/jedit, among
other things).
Thank you,
Talia
http://tlringer.github.io/
Email Gateway (Aug 22 2022 at 18:12):From: Buday Gergely <buday.gergely@uni-eszterhazy.hu>
Dear Talia,
https://ts.data61.csiro.au/projects/TS/proof-engineering/
is a good source for proof engineering using Isabelle.
Email Gateway (Aug 22 2022 at 18:12):From: Makarius <makarius@sketis.net>
On 07/08/18 01:47, Talia Ringer wrote:
I'm working on a proof engineering
<http://proofengineering.org/> survey paper. However, I don't have any
Isabelle expertise on the paper, and my community overwhelmingly skews
toward Coq users. To make sure Isabelle gets adequate coverage, I have been
consulting other people.
The term "proof engineering" is rarely used in the Isabelle community,
although people are probably doing it implicitly all the time. From the
perspective of the prover platform, the strategy has always been to make
it perform sufficiently well, such that high-end applications are easily
processed by it without requiring further adhoc tools.
There has always been a race of system infrastructure vs. applications.
A current snapshot of it is sketched in my presentation at the Isabelle
Workshop 2018: "Further Scaling of Isabelle Technology" (slides and
paper) https://sketis.net/2018/slides-for-presentations-at-floc-2018-oxford
The slides classify time scales for processing Isabelle theory sessions
as follows:
* instantaneous: 10 min (Edmund Stoiber constant)
* online waiting: 45 min (Paris Commuter constant)
* offline waiting: 2 h (French Lunch time)
* too long: 8 h (Overnight job)
The best I have seen in recent months is as follows:
1) Intel Xeon 2 * 20 cores with SSD
* 2 min for the Isabelle/HOL image (the "standard prelude"), which is
already quite big
* 6 min for the main Isabelle/HOL libraries, including HOL and the
huge HOL-Analysis session
* 11 min for the full Isabelle distribution (libraries and examples)
* 36 min for Isabelle + AFP, excluding unusually slow sessions
2) AMD 8 * 8 cores cluster
* 65 min for Isabelle + AFP, including regular slow sessions,
excluding some special very-slow sessions (one of it takes 4-6h)
I'm aware of the AFP,
but please don't hesitate to link to particular developments within the AFP
if you think they're especially noteworthy. It is OK to send your own work
if you think it is noteworthy and want to make sure it isn't missed.
I see AFP as the main application of Isabelle, and guess that it covers
approx. 60% of the visible Isabelle universe. Already since 2006,
Isabelle technology enhancements are driven by the requirements of AFP.
to give an idea of what sorts of things are
relevant, we already talk about Isar, the Isabelle style guide, Nominal
Isabelle, Transfer and Lifting, sledgehammer, and Isabelle/jedit, among
other things.
Note on Isar: well-structured proofs are not only better for the human
reader (and maintainer), but also for overall system performance. People
sometimes think that "declarative proof languages" are expensive
concerning automated proof search, but Isar is not called "declarative"
and its built-in automation is minimal: Isar means "Intelligible
semi-automated reasoning". Consequently, checking well-structured Isar
proofs is much faster than old-style "apply" scripts (this a minority
style in Isabelle applications, but a majority style in Coq applications).
Note on Eisbach: this proof method language has been added in recent
years. Inspired by Ltac, it allows to define Isar proof methods in the
source notation of the proof language. Some Eisbach spin-off concepts
allow to structure old-style apply-scripts, e.g. the 'subgoal' command
(similar to Coq bullets, but leading to parallel proofs). Beyond that it
is easy to define proof methods in Isabelle/ML: unlike Coq with its
separate "plugin" concept, Isabelle tools are defined directly within
the theory source, and subject to the normal interaction model (and
Prover IDE support).
Note on Isabelle/jEdit (in that spelling): this is the main front-end of
Isabelle/PIDE --- the Prover IDE framework --- and the default
user-interface of Isabelle. Another PIDE front-end is Isabelle/VSCode,
which is included in Isabelle2018 at a relatively modest 1.1 version,
but some people have already started using it. Isabelle users
occasionally abuse the name of the "jEdit" text editor for the whole
technology stack behind the Isabelle/jEdit product. Conceptually, the
key things are Isabelle/Scala and Isabelle/PIDE: a hybrid of Scala and
ML modules to support IDE concepts natively in the prover.
In recent years there has been a tendency to integrate more and more
prover technology into the Prover IDE (according to its name and
principle). A notable exception is the "isabelle build" command-line
tool, but it will also move into the IDE eventually.
The build tool understands the syntax of Isabelle theory sessions. This
is important for scaling, and "engineering" of large proof projects: the
system can impose certain policies according to the theory structure.
Taking away the free choice of "make" tools from the user also means
that Isabelle projects can easily build on existing projects, without
having to worry about the underlying project management technology: it
is just standard Isabelle itself.
Makarius
Email Gateway (Aug 22 2022 at 18:12):From: Makarius <makarius@sketis.net>
Non-Bavarians often don't understand the Edmund Stoiber joke above. Here
is the original speech https://www.youtube.com/watch?v=VY9bIZ9Jn9E as
representative of the many variations on the theme on Youtube. The
illustrations also help to get the point, despite Stoiber's strange way
of speaking German. (It is about building a high-speed train connection
from Munich main station to Munich airport, in order to get there in
max. 10 min. The project has not materialized so far.)
Related to that is the keynote by Peter O'Hearn at FLoC 2018 about
"Continuous Reasoning: Scaling the Impact of Formal Methods"
https://easychair.org/smart-program/FLoC2018/2018-07-09.html
He was talking about "diff time" of max. 15 min. It is the time you are
ready to invest to study the diff of an incoming changeset, to discuss
it with colleagues, decide to apply it or ignore it. His message to
formal-method tool builders: you need to be quicker than 15 min for
immediate formal analysis, if you want software developers to take your
results into account.
For formal proof checking the situation is analogous, but re-checking of
proofs is not optional, it cannot be ignored. Thus it is important to
have the main libraries and applications build in less than 10-15min in
order to remain productive in continued maintenance of the core system
and libraries.
Makarius
Last updated: Apr 26 2024 at 08:19 UTC