\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
%\usepackage[all]{xypic}
\usepackage{alltt}
\usepackage{url}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.6}
\definecolor{slidegreen}{rgb}{0,.4,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\definecolor{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.8,.8}
\definecolor{slideorange}{rgb}{1,.5,0}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\def\lightgray#1{\textcolor{slidelightgray}{#1}}
\def\darkgray#1{\textcolor{slidedarkgray}{#1}}
\def\orange#1{\textcolor{slideorange}{#1}}
\newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.1cm}}\vss}\strut}
\newpagestyle{fw0}{}{}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\xslidetitle}[1]{{\textcolor{slidered}{\strut\textbf{#1}}}\par
\vspace{-1.2em}{\color{white}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.8pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-20em}$}

\def\headphoto#1{\vbox to 0pt{
\vspace{-0.9em}
\hfill\includegraphics[width=6.5em]{/home/freek/talks/lagrange/pics/people/#1.eps}\par
\vss}\vspace{-1.4em}}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large\strut three wishes}

\red{Freek Wiedijk} \\
Radboud University Nijmegen
\smallskip

\green{future of ITP workshop} \\
University of Cambridge \\
{\small 2009\hspace{3pt}08\hspace{3pt}24, 09\hspace{1.6pt}:\hspace{1.5pt}30}

\end{slide}

\begin{slide}
\sectiontitle{why wish?}
\slidetitle{why ITP?}

\adviwait
\begin{itemize}
\item[$\bullet$]
\textsl{for mathematics}
\smallskip

\begin{itemize}
\advirecord{a1}{
\item
correctness
}

\advirecord{a2}{
\item
explicitness
}

\advirecord{a3}{
\item
\green{
mathematical objects in the physical world
}
}

\end{itemize}
\bigskip

\item[$\bullet$]
\textsl{for programming}
\smallskip
\adviwait
\adviplay{a1}
\adviwait
\adviplay{a2}
\adviwait
\adviplay{a3}
\adviwait

\begin{itemize}
\item
correctness \adviwait $\approx$ no bugs
\adviwait

\item
\red{carefree} programming
\adviwait

\item
\green{the \textsl{pleasure} of crafting a fully correct program}

\end{itemize}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\adviembed{xvieww /home/freek/talks/wishes/pics/tigergod.jpg}\adviwait[1]%
\sectiontitle{wishes for mathematics}
\slidetitle{\advirecord{b1}{\textsl{almost-wish}\exclspace:$\,$ ITP I can sell to the mathematicians}}
\adviwait\adviplay[slideblue]{b1}\vspace{-1.44em}\adviwait

\begin{itemize}
\item[$\bullet$]
strong and user programmable \red{\advirecord{c8}{automation}}\adviplay{c8} \green{\advirecord{c1}{({\small HOL})}}
\adviwait

\item[$\bullet$]
integrated \red{\advirecord{c9}{declarative proofs}}\adviplay{c9} and tactic scripts \green{\advirecord{c2}{(Isabelle)}}
\adviwait

\item[$\bullet$]
full \red{\advirecord{c10}{classical}}\adviplay{c10} {\small ZFC} style set theory \green{\advirecord{c3}{(Mizar)}}
\adviwait

\item[$\bullet$]
\red{\advirecord{c11}{partiality}}\adviplay{c11} taken seriously \green{\rlap{\white{\advirecord{c4a}{(B)}}}\advirecord{c4}{({\small PVS})}}\hfill \blue{\advirecord{c12}{$\left({1\over 0}\right)^2 \ge 0$}}
\adviwait

\item[$\bullet$]
dependent and empty types \green{\advirecord{c5}{(Coq)}}
\adviwait

\item[$\bullet$]
small kernel implementing small foundations \green{\rlap{\white{\advirecord{c6a}{({\small HOL})}}}\advirecord{c6}{(Metamath)}}
\adviwait

\item[$\bullet$]
mathematical and programming language identical \green{\advirecord{c7}{({\small ACL2})}}\toolong
\adviwait
\adviplay[slidegreen]{c1}
\adviwait
\adviplay[slidegreen]{c2}
\adviwait
\adviplay[slidegreen]{c3}
\adviwait
%\adviplay[slidegreen]{c4a}
%\adviwait
%\adviplay[white]{c4a}
\adviplay[slidegreen]{c4}
\adviwait
\adviplay[slidegreen]{c5}
\adviwait
\adviplay[slidegreen]{c6a}
\adviwait
\adviplay[white]{c6a}
\adviplay[slidegreen]{c6}
\adviwait
\adviplay[slidegreen]{c7}
\adviwait
\adviplay[slidered]{c8}
\adviwait
\adviplay[slidered]{c9}
\adviwait
\adviplay[slidered]{c10}
\adviwait
\adviplay[slidered]{c11}
\adviwait
\adviplay[slideblue]{c12}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textsl{almost-wish}\exclspace:$\,$ DNA for formal math}
\vspace{-1.44em}\adviwait

\begin{itemize}
\item[$\bullet$]
type theoretical lambda terms
\adviwait

\item[$\bullet$]
traces of {\small HOL} derivations
\adviwait

\item[$\bullet$]
LF
\adviwait

\item[$\bullet$]
de Bruijn's \red{$\Delta\Lambda$}, aka $\Lambda\Delta$, aka {\small AUT-SL}
$$\blue{{\cal T} ::= * \mathrel{|} x \mathrel{|} (\lambda x{\,:\,}{\cal T}.\, {\cal T}) \mathrel{|} ({\cal T}{\cal T})}$$
identification of $\lambda$ and $\Pi$\adviwait, no definitions or let-bindings \\
\adviwait
\green{unlabeled graphs with four kinds of nodes and two kinds of edges}
%\smallskip
\adviwait

\item[$\bullet$]
\textsl{{weaker version} of $\Delta\Lambda$}
%\adviwait

\red{no convertibility check} \\
\adviwait
{no difference between definitional equality and `book equality'}

\end{itemize}

\vspace{-2pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\textsl{almost-wish}\exclspace:$\,$ categories in {\small ZFC} style set theory}
\begin{center}
\bigskip
\textbf{problem:} \\
`the category of groups' is not a set
\end{center}

\begin{center}
\bigskip
how to talk about \red{`large categories'} in {\small ZFC} style set theory?
\end{center}
\adviwait

\vfill
\begin{center}
\green{(\green{`universes'} are not a nice solution)}
\end{center}

\end{slide}

\begin{slide}
\slidetitle{\textsl{almost-wish}\exclspace:$\,$ `very large scale formalization' project}

\begin{itemize}
\item[$\bullet$]
\red{all} of {undergraduate mathematics}
\smallskip
\adviwait

\green{will take about 140 $\mbox{man}\cdot\mbox{years}$}
\end{itemize}
\adviwait
\medskip

\blue{or:}
\medskip

\begin{itemize}
\item[$\bullet$]
\red{classification of finite simple groups}
\end{itemize}
\medskip

\blue{or:}
\medskip

\begin{itemize}
\item[$\bullet$]
\red{Fermat}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textsl{almost-wish}\exclspace:$\,$ formal library infrastructure}
\vspace{-1.44em}\adviwait

\begin{itemize}
\item[$\bullet$]
\textsl{made by a whole community, but \red{not well integrated}}

\begin{itemize}
\item
Coq's contribs

\item
Isabelle's {\small AFP}

\item
Mizar's {\small MML}

\end{itemize}
\adviwait

\item[$\bullet$]
\textsl{beautifully integrated, but \red{made by an isolated genius}}

\begin{itemize}
\item
John Harrison's {\small HOL} Light library

\item
Georges Gonthier's Ssreflect library
\adviwait

\end{itemize}
\end{itemize}
\medskip
\smallskip

Nijmegen's \blue{{MathWiki project}} just started \\
1 postdoc + 1 PhD student

\green{`Wikipedia for math' + formalizations + `Proof General on the Web'} \\
{Coq + Isabelle + \white{\rlap{\advirecord{d3}{{\small HOL} + \dots}}\rlap{\advirecord{d1}{Mizar + \dots}}}\rlap{\advirecord{d2}{\dots}}\adviplay{d1}\adviwait\adviplay[white]{d1}\adviplay{d2}\adviwait\adviplay[white]{d2}\adviplay{d3}}

\vspace{-14pt}
\vfill
\end{slide}


\begin{slide}
\slidetitle{genie, \textsl{my first wish}\exclspace:$\,$ better automation}
\vspace{-1.44em}\adviwait

\blue{progress in proof assistant technology\exclspace:}
\begin{itemize}
\item[$\bullet$]
automation of formalized \green{primary school} math = `arithmetic'

\item[$\bullet$]
\red{\advirecord{e1}{automation of formalized \advirecord{e2}{high school}\adviplay[slidegreen]{e2} math}}\adviplay{e1} = `calculus'

\item[$\bullet$]
automation of formalized \green{university} math

\end{itemize}
\adviwait
\adviplay[slidered]{e1}
\adviplay[slidered]{e2}

\begin{center}
\medskip\smallskip
\red{\texttt{HIGH\char`\_SCHOOL\char`\_STUDENT\char`\_TAC}}\adviwait \\
\green{\advirecord{e3}{`computer algebra under hypotheses'}}
$$\blue{x \ne 0 \;\land\; \big|\ln |x|\big| > 2 \;\land\, \int_0^{|x|} t\, dt \le 1 \;\;\Rightarrow\;\; -{1\over e^2} < x < {1\over e^2}}\medskip\adviwait\adviplay[slidegreen]{e3}\adviwait$$
\end{center}

{should run in less than a second \\
should run without any arguments}

%without references:
%\begin{itemize}
%\item[$\bullet$]
%assumptions in the goal = local labels in the proof
%
%\item[$\bullet$]
%theorems from the formal library
%
%\end{itemize}

\vspace{-12pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{wishes for programming}
\slidetitle{\textsl{almost-wish}\exclspace:$\,$ self-verified ITP}

\begin{itemize}
\item[$\bullet$]
\textbf{Coq in Coq}

\green{Bruno Barras}

\advirecord{f1}{not about the code of the actual system}
\medskip

\item[$\bullet$]
\textbf{{\small HOL} in {\small HOL}}

\green{John Harrison}
\adviwait\adviplay{f1}

about the \red{code of the actual system}\adviwait, but \adviwait currently
\smallskip

\begin{itemize}
\item
code has been a bit simplified (no definitions/polymorphism)
\adviwait
\item
no formal relation between OCaml code and its {\small HOL} rendering
\adviwait
\item
no proofs about parsing/printing \green{(Randy's complaint)}
\end{itemize}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{genie, \textsl{my second wish}\exclspace:$\,$ system for proving ML correct}

\red{miniML++}\adviwait
\bigskip

\textsl{features beyond Coq\exclspace:}
\adviwait
\begin{itemize}
\item[$\bullet$]
exceptions
\adviwait

\item[$\bullet$]
state
\adviwait

(just global \texttt{ref} variables is enough)
\adviwait

\item[$\bullet$]
non-terminating functions
\adviwait

\green{(my computer has a \texttt{\char`\^C} !)}
\adviwait

\item[$\bullet$]
input/output\adviwait \\ other {\small OS} related functions

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textsl{almost-wish\exclspace:$\;$} \rlap{\white{\advirecord{g1}{system for proving C correct}}}\advirecord{g2}{\red{nice} system for proving C correct}}
\vspace{-1.44em}\adviplay[slideblue]{g1}\adviwait\adviplay[white]{g1}\adviplay[slideblue]{g2}\adviwait

\textsl{philosophical question:}
what should I imagine `correctness' of
\begin{itemize}
\item[$\bullet$]
{\small \LaTeX}

\item[$\bullet$]
Mozilla

\end{itemize}
to mean?
\bigskip
\adviwait

\blue{from the quotes file\exclspace:}
\begin{quote}
\begin{alltt}
\green{V7 /bin/mail source: 554 lines.
1989 X.400 specs: 2200+ pages.}
\end{alltt}
\end{quote}
\bigskip
\adviwait

a program and a specification are the same kind of thing? \adviwait \\
\textsl{so what does it mean to prove a specification correct?}

\vfill
\end{slide}

%\begin{slide}
%\slidetitle{\textsl{example}\exclspace:$\,$ verified LF in C}
%
%Automath ($\approx$ LF) checker: \green{about 3100 lines of C}
%\adviwait
%\bigskip
%
%\blue{variable binding approaches:}
%
%\begin{enumerate}
%\item
%name
%
%\item
%nameless dummy = de Bruijn index
%
%\item
%{\small HOAS} = higher order abstract syntax
%\adviwait
%
%\item
%\textsl{pointer} to the object that represents the binder
%
%\red{terms as a graph in the heap}
%\adviwait
%
%\end{enumerate}
%\bigskip
%
%\green{are my algorithms for this representation correct?}
%
%\vfill
%\end{slide}

\begin{slide}
\slidetitle{genie, \textsl{my third wish}\exclspace!$\,$ system for proving strict conformance}
\vspace{-1.44em}\adviwait

\red{strictly conforming} = \\
\textsl{program runs the same on all machines} = \\
no undefined behavior, no \blue{\advirecord{h1}{unspecified}}\adviplay{h1} behavior
\medskip
\adviwait

\begin{itemize}
\item[$\bullet$]
no dereferenced {\small\texttt{NULL}} pointers
\vspace{-\smallskipamount}

\item[$\bullet$]
no dereferenced dangling pointers
\vspace{-\smallskipamount}

\item[$\bullet$]
no array accesses outside the bounds
\vspace{-\smallskipamount}

\item[$\bullet$]
no meaningless casts
\vspace{-\smallskipamount}

\item[$\bullet$]
\blue{\advirecord{h2}{no integer overflow}}\adviplay{h2}
\vspace{-\smallskipamount}

\item[$\bullet$]
no dependence on evaluation order \hfill $\,$\green{\texttt{i = i++;}}$\,$
\vspace{-\smallskipamount}

\item[$\bullet$]
\textsl{etcetera}

\end{itemize}
\medskip
\adviwait
\adviplay[slideblue]{h1}
\adviplay[slideblue]{h2}
\adviwait

\green{proving correctness without specification}

\vspace{-10pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{why wish?}
\slidetitle{needed?}

\begin{itemize}
\item[$\bullet$]
\textbf{first wish} (automated high school mathematics)

\green{computer algebra under hypotheses}
\medskip

\item[$\bullet$]
\textbf{second wish} (ML verification)

\green{Hoare logic for higher order programs in the presence of side effects}
\medskip

\item[$\bullet$]
\textbf{third wish} (C strict conformance)

\green{Hoare logic for proving strict conformance}

\end{itemize}
\adviwait
\adviembed{xvieww /home/freek/talks/wishes/pics/wishes.jpg}

\vfill
\end{slide}

\end{document}