Hacker News Reader

Comment by tehmillhouse | Hacker News Reader

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 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.)

View on HN

>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).

>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.

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

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.

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.

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.

> 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> and Scala <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.

I agree with most things you said, however.

> Lean is written in pretty principled C++.

For how long this will last? Many will agree here, that C++ is known for its ineptitude for "long-term" projects where maintenance issues are of crucial importance. I presume that proof assistants belong to that class. If Leo is the only developer of this project for the rest of life, then it is OK, I guess.

That's a reasonable concern. If Leo got hit by a bus the code quality would certainly suffer. He's pretty good about cleaning up PRs etc after merge, by which I mean, even if he isn't the only developer right now he does a lot of work to make sure the C++ code is up to snuff.

For me, C++ as its implementation language is one of the most promising things, as I suspect it's a significant reason why it's so much faster to check things than Idris. The speed difference is significant enough that I prefer it over Idris in spite of Idris' broader feature set: <1 second vs 10 seconds makes a huge difference to workflow when proving small lemmas (although it's possible I've somehow set up Idris wrong).

I would love Lean to become both reliable and fast tool. I suggest, it is in its infancy right now to judge it seriously. As for now, I would rather invest in well established tools.

I'm a fan of both sides of the Coq and Isabelle/HOL activities. I'm keeping an eye on CertiCoq. Right now, though, Isabelle/HOL seems to be ahead with work like Myreen and Davis's in terms of verified stacks:

https://www.cl.cam.ac.uk/~mom22/

This data structure refinement with one version getting automated to a large degree:

https://www21.in.tum.de/~lammich/pub/cpp2016_impds.pdf

Thanks to DeepSpec, Coq might exceed that in some ways:

https://deepspec.org/main

Note that a lot of work around Coq goes through CompCert which is proprietary software with restrictions on how it's used if one doesn't pay. The Isabelle/HOL alternatives like Simpl/C and CakeML are free software. Then, outside those two, we got a bunch of work being done in Maude (esp K Framework) with one an executable, formal semantics for C done like a compiler:

https://github.com/kframework/c-semantics

> 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?).

No, it's not true, it "extracts" (compiles) to C++. <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.

Reply on news.ycombinator.com