[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [O] Leslie Lamport has a foot in the 21st century
|
From: |
Clément Pit--Claudel |
|
Subject: |
Re: [O] Leslie Lamport has a foot in the 21st century |
|
Date: |
Tue, 11 Oct 2016 11:23:06 -0400 |
|
User-agent: |
Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0 |
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).
signature.asc
Description: OpenPGP digital signature