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
