6 ms·

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

134 points by pharrington 9y ago

pharrington 9y ago
The source repo is at https://github.com/JBakouny/Scallina https://github.com/JBakouny/Scallina
unboxed_type 9y ago
I wonder why they have not used Coq's extraction approach?
- gsps 9y 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_type 9y 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 :-)
    - nickpsecurity 9y ago
      When I read that, I thought "What a huge TCB versus what's typical." Additionally, there exist verified strategies for parsing that might be applicable to Scala. Depends on if their formalisms can handle the language's grammar or whatever. Additionally, if they write untrusted parts in ML, they can supplant it with stuff like property-based testing or CakeML compiler.
amelius 9y ago
I didn't read the paper, but is this restricted to purely functional programs?
- unboxed_type 9y ago
  Correct.
- sn9 9y ago
  It's a quick read. Only 2 pages. Not particularly dense and accessible to most programmers.
tehmillhouse 9y 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 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.
mathgenius 9y ago
It seems like this is the sort of thing that blockchain languages should be built on top of. Things like Etherium.
- carterschonwald 9y ago
  Working on something like this for work.

134 points by pharrington 9y ago

pharrington 9y ago

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

unboxed_type 9y ago

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

gsps 9y 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_type 9y 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 :-)
  - nickpsecurity 9y ago
    When I read that, I thought "What a huge TCB versus what's typical." Additionally, there exist verified strategies for parsing that might be applicable to Scala. Depends on if their formalisms can handle the language's grammar or whatever. Additionally, if they write untrusted parts in ML, they can supplant it with stuff like property-based testing or CakeML compiler.

amelius 9y ago

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

unboxed_type 9y ago
Correct.
sn9 9y ago
It's a quick read. Only 2 pages. Not particularly dense and accessible to most programmers.

tehmillhouse 9y 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 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.

mathgenius 9y ago

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

carterschonwald 9y ago
Working on something like this for work.