[Top][All Lists]

[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 

Attachment: signature.asc
Description: OpenPGP digital signature

reply via email to

[Prev in Thread] Current Thread [Next in Thread]