7 ms·

If you're interested in this kind of thing, note that Coq can also extract code in Haskell, Scheme and OCaml. If Coq's not quite your cup of tea, Isabelle/HOL

If you're interested in this kind of thing, note that Coq can also extract code in Haskell, Scheme and OCaml. If Coq's not quite your cup of tea, Isabelle/HOL is another proof assistant with amazing (dare I say superior?) tooling and automation, and it supports code extraction in SML, OCaml, Haskell and Scala. Microsoft Research's Lean theorem prover is also promising in this regard. Work is almost complete on native code compilation (via C code extraction), allowing you to compile all the constructions you can formalize in Lean directly to native code. (see https://github.com/leanprover/lean/pull/1241 https://github.com/leanprover/lean/pull/1241 for progress) (Note that none of those code extractors are verified to be correct themselves, lacking a formalization of the target language's semantics. You don't get a mathematical proof that the code you're running does what you specified, but you get pretty damn close.)

tom_mellior 9y ago
> native code compilation (via C code extraction), allowing you to compile all the constructions you can formalize in Lean directly to native code Is that really true? What do they do for garbage collection, do they provide their own or use something like the Boehm collector? As far as I understood, F* also allows C extraction, but only for a subset not including dynamic allocation (or maybe with explicit memory management via effects?).
- cmrx64 9y ago
  No, it's not true, it "extracts" (compiles) to C++. <https://github.com/leanprover/lean/pull/1241> https://github.com/leanprover/lean/pull/1241> It's written in Lean itself, as a metaprogram. The code it generates calls into the Lean library ("runtime") for some objects, otherwise uses native types when it can. vm_obj's in Lean are reference counted. There's also in-progress work on an LLVM backend.
unboxed_type 9y ago
>Note that none of those code extractors are verified to be >correct themselves, lacking a formalization of the target >language's semantics. CertiCoq project aims to provide a certified compiler from Coq into CLight (formalized subset of "Safe C"). In this respect, it is superior to what you have mentioned, I guess. Offtopic: Lean's effort seems strange to me. Usage of C++ as its implementation language gets me really nervous, I feel doubt in its reliability.
- hardlianotion 9y ago
  What is acceptable to use in your view? In my own, if you don't like C++, you can't like Scala much and I am a fan of both
  - lmm 9y ago
    I don't think they're that similar? I dislike C++ because of its large amount of unsafe constructs and huge number of special-cased language-level features; I like Scala because it's the most practical language I've found for writing safe enough code and because the core language is quite small, with many features moved out into libraries or patterns of combining simpler features.
    - hardlianotion 9y ago
      They are both multi-paradigm languages with plenty of modes of expression. Both provide sufficient ways to hurt yourself. There are enough Scala implementation warts to trap the unwary. edit - in my parent comment I should have restricted scope of the comment to the use of the language for this purpose.
  - unboxed_type 9y ago
    Scala is different in that it has stronger type system, automatic memory management, the language is well-specified and is based on JVM, a reliable runtime. I would suggest that even Java would be much better choice than C++ for that project.
- cmrx64 9y ago
  > Offtopic: Lean's effort seems strange to me. Usage of C++ as its implementation language gets me really nervous, I feel doubt in its reliability. Not only is this unfounded, it's unreasonable. I can interpret "reliability" in two ways: 1. The tool crashes a lot This isn't true in practice, and it throws an exception with about the same frequency that Isabelle throws an ML exception, for me. I haven't observed any segfaults but they do happen sometimes (and are usually fixed quickly, Leo is really awesome). Lean is written in pretty principled C++. 2. You don't feel safe trusting it when it says it proves something Any tool worth its salt in this space satisfies the "de Bruijn criterion" -- can have a small, independent checker. In this case, Lean's kernel is the calculus of inductive constructions with a non-cumulative hierarchy of universes, and there exist independent typecheckers written in Haskell <https://github.com/leanprover/tc> https://github.com/leanprover/tc> and Scala <https://github.com/gebner/trepplein> https://github.com/gebner/trepplein>. I have an in-progress one written in Rust as well. Meanwhile, Lean is quite fast, the metaprogramming is lovely, and there are some really awesome tools in the pipeline.
logicchains 9y ago
>If Coq's not quite your cup of tea, Isabelle/HOL is another proof assistant with amazing (dare I say superior?) tooling and automation, and it supports code extraction in SML, OCaml, Haskell and Scala. I'll just note that Isabelle/HOL does not support dependent types, a trade-off it makes in exchange for superior automation (including excellent SMT solver integration). This makes it less suitable for some styles of proving than Coq, Agda, Idris and Lean. I suspect people coming from Coq are less likely to notice this however, as dependent types seem to be used less in Coq than in e.g. Agda or Idris due to the poor support for dependent pattern matching making some things unnecessarily difficult (although this situation is improving with every release).

tom_mellior 9y ago

> native code compilation (via C code extraction), allowing you to compile all the constructions you can formalize in Lean directly to native code Is that really true? What do they do for garbage collection, do they provide their own or use something like the Boehm collector? As far as I understood, F* also allows C extraction, but only for a subset not including dynamic allocation (or maybe with explicit memory management via effects?).

cmrx64 9y ago
No, it's not true, it "extracts" (compiles) to C++. <https://github.com/leanprover/lean/pull/1241> https://github.com/leanprover/lean/pull/1241> It's written in Lean itself, as a metaprogram. The code it generates calls into the Lean library ("runtime") for some objects, otherwise uses native types when it can. vm_obj's in Lean are reference counted. There's also in-progress work on an LLVM backend.

unboxed_type 9y ago

>Note that none of those code extractors are verified to be >correct themselves, lacking a formalization of the target >language's semantics. CertiCoq project aims to provide a certified compiler from Coq into CLight (formalized subset of "Safe C"). In this respect, it is superior to what you have mentioned, I guess. Offtopic: Lean's effort seems strange to me. Usage of C++ as its implementation language gets me really nervous, I feel doubt in its reliability.

hardlianotion 9y ago
What is acceptable to use in your view? In my own, if you don't like C++, you can't like Scala much and I am a fan of both
- lmm 9y ago
  I don't think they're that similar? I dislike C++ because of its large amount of unsafe constructs and huge number of special-cased language-level features; I like Scala because it's the most practical language I've found for writing safe enough code and because the core language is quite small, with many features moved out into libraries or patterns of combining simpler features.
  - hardlianotion 9y ago
    They are both multi-paradigm languages with plenty of modes of expression. Both provide sufficient ways to hurt yourself. There are enough Scala implementation warts to trap the unwary. edit - in my parent comment I should have restricted scope of the comment to the use of the language for this purpose.
- unboxed_type 9y ago
  Scala is different in that it has stronger type system, automatic memory management, the language is well-specified and is based on JVM, a reliable runtime. I would suggest that even Java would be much better choice than C++ for that project.
cmrx64 9y ago
> Offtopic: Lean's effort seems strange to me. Usage of C++ as its implementation language gets me really nervous, I feel doubt in its reliability. Not only is this unfounded, it's unreasonable. I can interpret "reliability" in two ways: 1. The tool crashes a lot This isn't true in practice, and it throws an exception with about the same frequency that Isabelle throws an ML exception, for me. I haven't observed any segfaults but they do happen sometimes (and are usually fixed quickly, Leo is really awesome). Lean is written in pretty principled C++. 2. You don't feel safe trusting it when it says it proves something Any tool worth its salt in this space satisfies the "de Bruijn criterion" -- can have a small, independent checker. In this case, Lean's kernel is the calculus of inductive constructions with a non-cumulative hierarchy of universes, and there exist independent typecheckers written in Haskell <https://github.com/leanprover/tc> https://github.com/leanprover/tc> and Scala <https://github.com/gebner/trepplein> https://github.com/gebner/trepplein>. I have an in-progress one written in Rust as well. Meanwhile, Lean is quite fast, the metaprogramming is lovely, and there are some really awesome tools in the pipeline.

logicchains 9y ago

>If Coq's not quite your cup of tea, Isabelle/HOL is another proof assistant with amazing (dare I say superior?) tooling and automation, and it supports code extraction in SML, OCaml, Haskell and Scala. I'll just note that Isabelle/HOL does not support dependent types, a trade-off it makes in exchange for superior automation (including excellent SMT solver integration). This makes it less suitable for some styles of proving than Coq, Agda, Idris and Lean. I suspect people coming from Coq are less likely to notice this however, as dependent types seem to be used less in Coq than in e.g. Agda or Idris due to the poor support for dependent pattern matching making some things unnecessarily difficult (although this situation is improving with every release).