Coq-based synthesis of Scala programs which are correct-by-construction [pdf]

https://cedric.cnam.fr/fichiers/art_4027.pdf

by pharrington • 9 years ago

134 25 9 years ago

cedric.cnam.fr

pharrington• 9 years ago

The source repo is at https://github.com/JBakouny/Scallina

unboxed_type7• 9 years ago

I wonder why they have not used Coq's extraction approach?

gsps• 9 years ago

As far as I understand, their approach is exactly that, i.e., another target language for extraction. Synthesis is a bit of an overloaded term.

unboxed_type7• 9 years ago

"The compiler itself is also written in Scala and its underlying Coq parser is largely based on the use of parser combinators"

while "true" extractor has to be written in Coq, as I understand :-)

amelius• 9 years ago

I didn't read the paper, but is this restricted to purely functional programs?

unboxed_type7• 9 years ago

Correct.

sn9• 9 years ago

It's a quick read. Only 2 pages. Not particularly dense and accessible to most programmers.

tehmillhouse• 9 years ago

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

tom_mellior• 9 years 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?).

cmrx643• 9 years ago

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.

unboxed_type7• 9 years 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.

hardlianotion2• 9 years 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

cmrx643• 9 years 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> 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.

logicchains2• 9 years ago

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

nickpsecurity2• 9 years ago

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

logicchains2• 9 years 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).

mathgenius• 9 years ago

It seems like this is the sort of thing that blockchain languages should be built on top of. Things like Etherium.

carterschonwald• 9 years ago

Working on something like this for work.

Coq-based synthesis of Scala programs which are correct-by-construction [pdf]

Related Stories