4 ms·
Look at idris - proofs are expressed using dependent types which allow full propositional logic and implementations exploit these proofs using a haskell like la
by shriphani 7y ago
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/ https://www.idris-lang.org/
- wuschel 7y agoThere 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/
- chalst 7y agoDependent type theory doesn't directly model the concepts of TLA+ (e.g., an eventually modality), so this doesn't really answer the question.
- deleted 7y ago[deleted]