From mboxrd@z Thu Jan 1 00:00:00 1970 From: =?UTF-8?Q?Cl=c3=a9ment_Pit--Claudel?= Subject: Re: Leslie Lamport has a foot in the 21st century Date: Tue, 11 Oct 2016 11:23:06 -0400 Message-ID: <108f5bab-3680-5c69-6812-4d1f57db28b0@gmail.com> References: <57F8B0F4.9090407@free.fr> <878ttxk39i.fsf@desiato.home.uhoreg.ca> <87pon9wki0.fsf@mbork.pl> <87vawzhr2z.fsf@desiato.home.uhoreg.ca> Mime-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha256; protocol="application/pgp-signature"; boundary="6rm3Jc5XDHqVgi91wWR1O9R8SAoeLRrAh" Return-path: Received: from eggs.gnu.org ([2001:4830:134:3::10]:36104) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1btytl-0007wg-0q for emacs-orgmode@gnu.org; Tue, 11 Oct 2016 11:23:22 -0400 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1btyte-0005mV-Tr for emacs-orgmode@gnu.org; Tue, 11 Oct 2016 11:23:19 -0400 Received: from mout.kundenserver.de ([212.227.126.134]:56399) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1btyte-0005ls-JH for emacs-orgmode@gnu.org; Tue, 11 Oct 2016 11:23:14 -0400 Received: from [18.189.6.80] ([18.189.6.80]) by mrelayeu.kundenserver.de (mreue003) with ESMTPSA (Nemesis) id 0MJoUy-1bssy52Jme-001DC2 for ; Tue, 11 Oct 2016 17:23:13 +0200 In-Reply-To: <87vawzhr2z.fsf@desiato.home.uhoreg.ca> List-Id: "General discussions about Org-mode." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: emacs-orgmode-bounces+geo-emacs-orgmode=m.gmane.org@gnu.org Sender: "Emacs-orgmode" To: emacs-orgmode@gnu.org This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --6rm3Jc5XDHqVgi91wWR1O9R8SAoeLRrAh Content-Type: multipart/mixed; boundary="pxJ2eLotWRmnR4nITLLHFSJSSxCwrE5VJ"; protected-headers="v1" From: =?UTF-8?Q?Cl=c3=a9ment_Pit--Claudel?= To: emacs-orgmode@gnu.org Message-ID: <108f5bab-3680-5c69-6812-4d1f57db28b0@gmail.com> Subject: Re: [O] Leslie Lamport has a foot in the 21st century References: <57F8B0F4.9090407@free.fr> <878ttxk39i.fsf@desiato.home.uhoreg.ca> <87pon9wki0.fsf@mbork.pl> <87vawzhr2z.fsf@desiato.home.uhoreg.ca> In-Reply-To: <87vawzhr2z.fsf@desiato.home.uhoreg.ca> --pxJ2eLotWRmnR4nITLLHFSJSSxCwrE5VJ Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable On 2016-10-11 10:56, Hubert Chathi wrote: > I suspect that it will be a long time before hierarchical proofs gain > much popularity though, given that Lamport has been talking about them > since at least the 90's, and I haven't seen one "in the wild" yet. Depends how much you're willing to stretch the definition. Many machine-= checked proofs are written in a pretty hierarchical style, and some of th= e associated tools support folding and expanding subproofs (see the middl= e gif in https://github.com/cpitclaudel/company-coq/#outlines-code-foldin= g-and-jumping-to-definition). --pxJ2eLotWRmnR4nITLLHFSJSSxCwrE5VJ-- --6rm3Jc5XDHqVgi91wWR1O9R8SAoeLRrAh Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQIcBAEBCAAGBQJX/QPaAAoJEPqg+cTm90wjdPEP/2002Y014+B0Kp29qM0fPBFS 3IIIoe3IPNRRTkQLWYLcCArFI8UuDABYjEFo/yUfXQwzQZ18OVZGVkadeGCbVHnS WL5QxwCZ09Y6aJh/P/j5dJcsak1WE5iwJBkiQhz0Skc870r14/VIFiIssY+c5+em EHYyEhmBr9qo0KZVfeMIuApVFStwesbPl5YtAPCOZnP4z0q1XFEtWOxvy7IixOwg 1c38HhAGHhdH2MGEmARyVZjPTz+5WPEtMyAQBO1N3/s98wab6Q7/UDw8BiRvKNw6 wedgMsMCiRgXW7afGggjIgxyjuhIGjsjWW3oCF2t9oY7huMmhcRfcCM3ZrbiMRVe uqGt5j7ZTrueWQq2jJ3nWTphgIpsxKpRyIk131vZOeyn0ikGRF0YpwJpOIOJX37W dIpepXyMXkZ1oy6XZSn94YN+1WF1QAEPOfaQkWv6Ud8fRlfUNsll5kzcez84BfQW grvOJIiX+jKIvETTW0wd8KGFUWwxxMHZT3o5g/m63IYQL1SAteRuIzV/a7n6VJgt vohiqGEV2hYq2ZndfJSEABZWj0Lk9QFrFsSaQC2A3WaYIKKpboe2/QSm3Lmaq0n0 9h9v+vD8ft9fl4S1hRh+98SzazQiAF+C2rwn2Q9XRgm69lHpYbQkyWQuUztzBKHo i275G41MbN+ljKgUuEdd =nbLG -----END PGP SIGNATURE----- --6rm3Jc5XDHqVgi91wWR1O9R8SAoeLRrAh--