News for hackers. Stuff that matters.

A comment on Writing correct lock-free and distributed stateful systems in Rust, with TLA+. Parent comment

Re:Writing correct lock-free and distributed stateful system... by dronemallone on Friday May 19, 2017 @09:41AM (#14375494)
That "facility" is the Curry-Howard correspondence!
[ Parent | on HN ]
Re:Writing correct lock-free and distributed stateful system... by mafribe on Friday May 19, 2017 @11:15AM (#14376471)
Not necessarily. Isabelle/HOL, an prover not based on CH but on the LCF-architecture, can also do program extraction, see e.g. Program extraction in Isabelle:

https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides....

[ Parent | on HN ]
Re:Writing correct lock-free and distributed stateful system... by samth on Friday May 19, 2017 @05:36PM (#14379533)
Extraction of terms written using Fixpoint isn't really the Curry-Howard correspondence. Instead, the correspondence is between (for example) proofs of correctness and terms in the Calculus of Constructions.

[Fixpoint terms are also CIC programs, so there's a sense in which they're related, but it's not really about Curry-Howard.]

[ Parent | on HN ]