Leslie Lamport has a foot in the 21st century

Leslie Lamport has a foot in the 21st century

[Thierry Banel]

Last week I attended a lecture by Leslie Lamport, author of LaTex:
"How to Write a 21st Century Proof".
His answer: write in a structured, hierarchical way.
At the deepest level lie obvious assertions on which the proof is built.

The best medium, he said, is hypertext.
Hypertext gives the ability to fold or show low details.
But wait... I know a about a software that just do that.
How is it called? Yes I remember: Emacs Org Mode.

He went on:
we should get rid of our 17th century habit of writing on dead trees.
PDF was designed for printing, and cannot do hypertext.

If I follow him, Org Mode should probably focus more on
Html (hypertext) export than on PDF-LaTex (paper).
I tried  both.
IMO PDF-LaTex is an order of magnitude more difficult than Html.
And I have already written papers in Tex & LaTex in the past.

In Html we have CSS, which gives us tons of flexibility.
We have Firebug to understand CSS.
We have MathJax to write maths in Html with LaTex quality standard.

In Org Mode we have a CSS starting point:
  http://orgmode.org/org.cssorg.css.
We have org-info-js which is easy to set up and pleasant to use:
  http://orgmode.org/worg/code/org-info-js/

But... Is Leslie killing LaTex?

Re: Leslie Lamport has a foot in the 21st century

[Grant Rettke]

On Sat, Oct 8, 2016 at 3:40 AM, Thierry Banel <tbanelwebmin@free.fr> wrote:
> But... Is Leslie killing LaTex?

No. LaTeX is a markup/programming-language and it /could/ be compiled
directly to whatever new ideal format arises, too.

Re: Leslie Lamport has a foot in the 21st century

[Thomas S. Dye]

Grant Rettke writes:

> On Sat, Oct 8, 2016 at 3:40 AM, Thierry Banel <tbanelwebmin@free.fr> wrote:
>> But... Is Leslie killing LaTex?
>
> No. LaTeX is a markup/programming-language and it /could/ be compiled
> directly to whatever new ideal format arises, too.

See http://tug.org/tex4ht/ which converts TeX's dvi output to HTML, XML,
braille, etc.

Tom

-- 
Thomas S. Dye
http://www.tsdye.com

Re: Leslie Lamport has a foot in the 21st century

[Hubert Chathi]

On Sat, 8 Oct 2016 10:50:09 -0500, Grant Rettke <gcr@wisdomandwonder.com> said:

> On Sat, Oct 8, 2016 at 3:40 AM, Thierry Banel <tbanelwebmin@free.fr> wrote:
>> But... Is Leslie killing LaTex?

> No. LaTeX is a markup/programming-language and it /could/ be compiled
> directly to whatever new ideal format arises, too.

It's not a matter of compiling to the right file format, but rather
whether LaTeX is the right tool for the type of document structure that
Lamport is proposing.  His system requires people to be able to expand
and collapse things, which TeX is unable to handle.  You might be able
to fake it in TeX by using hyperlinks, but that might drive the PDF/dead
tree readers crazy once they get a couple of levels deep in your proof,
having to keep track of all the links that they had to follow.  Not to
mention, it would probably require a lot of TeX black magic to
implement.  It would require adding some new environments and/or
commands to LaTeX, which the current LaTeX-to-HTML converters wouldn't
be able to handle -- you'd need to implement those bits.  So given that
you'd need to create a bunch of new infrastructure, and TeX would
basically just be dead weight, the question is: is it worth still using
LaTeX, or is it better to start with something else entirely that's
better suited to handle hierarchical proofs?

BTW, Lamport has been talking about hierarchical proofs since the early
90's
http://research.microsoft.com/en-us/um/people/lamport/pubs/lamport-how-to-write.pdf

BTW, Grant, if you're interested in different types of scientific
communication, you may be interested in Bret Victor's work, e.g.
http://worrydream.com/#!/ScientificCommunicationAsSequentialArt

-- 
Hubert Chathi - Email: hubert@uhoreg.ca - https://www.uhoreg.ca/
Jabber: hubert@uhoreg.ca - Matrix: @uhoreg:matrix.org
PGP/GnuPG key: 4096R/113A1368 (Key available at pool.sks-keyservers.net)
Fingerprint: F24C F749 6C73 DDB8 DCB8  72DE B2DE 88D3 113A 1368

Re: Leslie Lamport has a foot in the 21st century

[Marcin Borkowski]

On 2016-10-09, at 16:26, Hubert Chathi <hubert@uhoreg.ca> wrote:

> On Sat, 8 Oct 2016 10:50:09 -0500, Grant Rettke <gcr@wisdomandwonder.com> said:
>
>> On Sat, Oct 8, 2016 at 3:40 AM, Thierry Banel <tbanelwebmin@free.fr> wrote:
>>> But... Is Leslie killing LaTex?
>
>> No. LaTeX is a markup/programming-language and it /could/ be compiled
>> directly to whatever new ideal format arises, too.
>
> It's not a matter of compiling to the right file format, but rather
> whether LaTeX is the right tool for the type of document structure that
> Lamport is proposing.  His system requires people to be able to expand
> and collapse things, which TeX is unable to handle.  You might be able
> to fake it in TeX by using hyperlinks, but that might drive the PDF/dead
> tree readers crazy once they get a couple of levels deep in your proof,
> having to keep track of all the links that they had to follow.  Not to
> mention, it would probably require a lot of TeX black magic to
> implement.  It would require adding some new environments and/or
> commands to LaTeX, which the current LaTeX-to-HTML converters wouldn't
> be able to handle -- you'd need to implement those bits.  So given that
> you'd need to create a bunch of new infrastructure, and TeX would
> basically just be dead weight, the question is: is it worth still using
> LaTeX, or is it better to start with something else entirely that's
> better suited to handle hierarchical proofs?

Please be careful to make the distinction between TeX and LaTeX here.
Basically, LaTeX 2.09 *should* be dead, and LaTeX2e *is* dead weight to
some extent.  And you might want to ping the LaTeX team, who are working
on LaTeX3 (and the high level markup is still undecided at this point in
time - and it will probably be so for the next few years), about
Lamport's ideas and implementing them.

I don't remember exactly what Lamport has written about proofs (I read
it more than a year ago AFAIR), but isn't it true that what he proposes
is (from typographical point of view) just a (possibly hyperlinked) tree
structure?  If so, LaTeX should be perfectly suited as markup language,
and I would not expect a huge amount of work to implement the missing
bits (though I might be mistaken).  Of course, the hard part would be
the actual hide/show part; HTML+JS might be better suited to that
indeed.

I guess that using ConTeXt would a better route here.

Just my 2 cents.

Best,

-- 
Marcin Borkowski

Re: Leslie Lamport has a foot in the 21st century

[Thomas S. Dye]

Hubert Chathi writes:


> BTW, Grant, if you're interested in different types of scientific
> communication, you may be interested in Bret Victor's work, e.g.
> http://worrydream.com/#!/ScientificCommunicationAsSequentialArt

Many thanks for this link to Victor's interesting work.  His effective
use of many small graphics reminds me of Edward Tufte's book design,
which places small graphics in the margin in order to preserve the flow
of text.

All the best,
Tom

-- 
Thomas S. Dye
http://www.tsdye.com

Re: Leslie Lamport has a foot in the 21st century

[Hubert Chathi]

On Sun, 09 Oct 2016 18:32:55 +0200, Marcin Borkowski <mbork@mbork.pl> said:

> On 2016-10-09, at 16:26, Hubert Chathi <hubert@uhoreg.ca> wrote:

>> It's not a matter of compiling to the right file format, but rather
>> whether LaTeX is the right tool for the type of document structure
>> that Lamport is proposing.  His system requires people to be able to
>> expand and collapse things, which TeX is unable to handle.  You might
>> be able to fake it in TeX by using hyperlinks, but that might drive
>> the PDF/dead tree readers crazy once they get a couple of levels deep
>> in your proof, having to keep track of all the links that they had to
>> follow.  Not to mention, it would probably require a lot of TeX black
>> magic to implement.  It would require adding some new environments
>> and/or commands to LaTeX, which the current LaTeX-to-HTML converters
>> wouldn't be able to handle -- you'd need to implement those bits.  So
>> given that you'd need to create a bunch of new infrastructure, and
>> TeX would basically just be dead weight, the question is: is it worth
>> still using LaTeX, or is it better to start with something else
>> entirely that's better suited to handle hierarchical proofs?

> Please be careful to make the distinction between TeX and LaTeX here.

Yes, I was careful to distinguish between TeX and LaTeX, and I said
"TeX" when I meant "TeX".  I'm sure that LaTeX is perfectly capable of
representing Lamport's proposed proof structure.  But the question is,
why use LaTeX when half the reason for using LaTeX is that it can
generate beautiful printed output through TeX, and Lamport's
hierarchical proof would translate pretty badly to print.  (As I
mentioned, it would be possible to translated it to a printed version,
but reading a printed version would likely be rather painful.)

I don't know much about LaTeX3, but it looks like it's still targeting
print, and so it would have the same problems.  Not only that, but the
existing LaTeX-to-HTML tools might not work with LaTeX3, so if you're
getting rid of half of your toolset, why switch to LaTeX3 instead of
some other format that targets HTML more directly?

I'm sure that there may be good reasons for sticking with LaTeX
(e.g. being able to easily copy-and-paste into for-print articles,
familiarity with the language, etc.), but there are also disadvantages,
and it will be interesting to see what factors determine what type of
system, whether it be LaTeX or something closer to HTML, ends up being
used to write hierarchical proofs.

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.  So I
don't know how much of a factor it will be "killing" LaTeX, if LaTeX
ever does get killed.

-- 
Hubert Chathi - Email: hubert@uhoreg.ca - https://www.uhoreg.ca/
Jabber: hubert@uhoreg.ca - Matrix: @uhoreg:matrix.org
PGP/GnuPG key: 4096R/113A1368 (Key available at pool.sks-keyservers.net)
Fingerprint: F24C F749 6C73 DDB8 DCB8  72DE B2DE 88D3 113A 1368

Re: Leslie Lamport has a foot in the 21st century

[Clément Pit--Claudel]

[-- Attachment #1.1: Type: text/plain, Size: 587 bytes --]

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 the associated tools support folding and expanding subproofs (see the middle gif in https://github.com/cpitclaudel/company-coq/#outlines-code-folding-and-jumping-to-definition).


[-- Attachment #2: OpenPGP digital signature --]
[-- Type: application/pgp-signature, Size: 819 bytes --]

Re: Leslie Lamport has a foot in the 21st century

[Marcin Borkowski]

On 2016-10-11, at 16:56, Hubert Chathi <hubert@uhoreg.ca> wrote:

> I don't know much about LaTeX3, but it looks like it's still targeting
> print, and so it would have the same problems.  Not only that, but the
> existing LaTeX-to-HTML tools might not work with LaTeX3, so if you're
> getting rid of half of your toolset, why switch to LaTeX3 instead of
> some other format that targets HTML more directly?
>
> I'm sure that there may be good reasons for sticking with LaTeX
> (e.g. being able to easily copy-and-paste into for-print articles,
> familiarity with the language, etc.), but there are also disadvantages,
> and it will be interesting to see what factors determine what type of
> system, whether it be LaTeX or something closer to HTML, ends up being
> used to write hierarchical proofs.
>
> 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.  So I
> don't know how much of a factor it will be "killing" LaTeX, if LaTeX
> ever does get killed.

Well, one might think that after about 20 years, LaTeX 2.09 should be
already dead.  It's not.  Academia has a lot of inertia.  So we're
probably stuck with LaTeX2e (for better or for worse) for at least
several decades.

Best,

-- 
Marcin Borkowski

Re: Leslie Lamport has a foot in the 21st century

[Adonay Felipe Nogueira]

An interesting subject.

On sidenote, I'm writing an introduction guide to writting documents in
either Org mode or LaTeX, for writers, scientists and students
([1]). It's currently in Brazilian Portuguese, but of course I might
translate it to English and also accept contributions.

[1] <https://notabug.org/adfeno/Org_LaTeX_intro>.

Marcin Borkowski <mbork@mbork.pl> writes:

> Well, one might think that after about 20 years, LaTeX 2.09 should be
> already dead.  It's not.  Academia has a lot of inertia.  So we're
> probably stuck with LaTeX2e (for better or for worse) for at least
> several decades.
>
> Best,

-- 
- https://libreplanet.org/wiki/User:Adfeno
- Palestrante e consultor sobre /software/ livre (não confundir com
  gratis).
- "WhatsApp"? Ele não é livre. Por favor, veja formas de se comunicar
  instantaneamente comigo no endereço abaixo.
- Contato: https://libreplanet.org/wiki/User:Adfeno#vCard
- Arquivos comuns aceitos (apenas sem DRM): Corel Draw, Microsoft
  Office, MP3, MP4, WMA, WMV.
- Arquivos comuns aceitos e enviados: CSV, GNU Dia, GNU Emacs Org, GNU
  GIMP, Inkscape SVG, JPG, LibreOffice (padrão ODF), OGG, OPUS, PDF
  (apenas sem DRM), PNG, TXT, WEBM.