Learn TLA+ (2018)

Re:Learn TLA+ (2018) by shriphani on Sunday February 23, 2020 @01:39AM (#22395495)

Look at idris - proofs are expressed using dependent types which allow full propositional logic and implementations exploit these proofs using a haskell like language that allows imperative + purely functional code: https://www.idris-lang.org/

[ Parent | on HN ]

Re:Learn TLA+ (2018) by wuschel on Sunday February 23, 2020 @05:07AM (#22396050)

There are more: F* compiles to Ocaml/F#/C/ASM/WASM [1] and it's variant Low*, and ATS [2], which compiles to C.

  [1] https://www.fstar-lang.org/
  [2] http://www.ats-lang.org/

[ Parent | on HN ]

Re:Learn TLA+ (2018) by chalst on Sunday February 23, 2020 @09:42AM (#22397015)

Dependent type theory doesn't directly model the concepts of TLA+ (e.g., an eventually modality), so this doesn't really answer the question.

[ Parent | on HN ]