14
$\begingroup$

I am looking for proof assistants with which I can write sound proofs about my functions and values, as well as compile actions of type IO () into executable code. In other words, I am looking for a language which has support for theorem proving as well as general purpose programming.

With Coq, I can extract my Coq files into OCaml but it is not executable code because the code does not have any side effects. So, I cannot use Coq to write an executable pacman game, for example.

$\endgroup$
2
  • $\begingroup$ @GuyCoder all of these answers are interesting: I do not see how I could choose one answer as "the correct answer" $\endgroup$ Mar 2, 2022 at 15:35
  • $\begingroup$ I tried to indicate my (genuine) appreciation towards the answers by upvoting the answers I like. I think the "green check mark" communicates that a certain answer is the most correct/useful amongst all others. It is indeed a useful bit of annotation for certain questions, but I do not think this question should be viewed that way. $\endgroup$ Mar 2, 2022 at 15:53

4 Answers 4

15
$\begingroup$

You speak of program extraction, but if your main goal is to prove correctness of effectful programs, you might consider programming languages that allow you to write code directly, and prove it correct. Here are some options:

  • Idris has good support for computational effects and it uses dependent types a la proof assistants.

  • F* is a general-purpose functional programming language with effects aimed at program verification.

  • LiquidHaskell refines Haskell's types with logical predicates that let you enforce important properties at compile time.

If you prefer to stick to a proper proof assistant and extract code, then you still have some options:

  • Agda compilers lets you compile code to Haskell and Javascript (and it knows about effects)

  • Contrary to your claim that Coq can only extract pure code, it is possible to extract effectful code, see this answer for some pointers. The idea is that inside Coq we axiomatize the effects and then realize them with actual effectful code using the Extract Constant feature.

$\endgroup$
1
  • 2
    $\begingroup$ I would add github.com/coq-io as beautiful project for Coq extraction with System IO. $\endgroup$ Feb 8, 2022 at 23:35
11
$\begingroup$

Lean 4 is both a proof assistant and general-purpose programming language, with built-in native code generation.

# use pinned version of the Lake package manager via `elan`
$ lake +leanprover/lean4:v4.0.0-m3 init hello

$ cat Main.lean
import Hello

def main : IO Unit :=
  IO.println s!"Hello, {hello}!"

$ lake build
> LEAN_PATH=./build/lib /home/sebastian/.elan/toolchains/leanprover--lean4---nightly/bin/lean ././Hello.lean -R ./. -o ./build/lib/Hello.olean -i ./build/lib/Hello.ilean -c ./build/ir/Hello.c
> /home/sebastian/.elan/toolchains/leanprover--lean4---nightly/bin/leanc -c -o ./build/ir/Hello.o ./build/ir/Hello.c -O3 -DNDEBUG
> LEAN_PATH=./build/lib /home/sebastian/.elan/toolchains/leanprover--lean4---nightly/bin/lean ././Main.lean -R ./. -o ./build/lib/Main.olean -i ./build/lib/Main.ilean -c ./build/ir/Main.c
> /home/sebastian/.elan/toolchains/leanprover--lean4---nightly/bin/leanc -c -o ./build/ir/Main.o ./build/ir/Main.c -O3 -DNDEBUG
> /home/sebastian/.elan/toolchains/leanprover--lean4---nightly/bin/leanc -o ./build/bin/hello ./build/ir/Main.o ./build/ir/Hello.o

$ file ./build/bin/hello
./build/bin/hello: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /nix/store/41dj1v3qz9a5kjncpkxhmq50yg9r24dn-glibc-2.33-62/lib/ld-linux-x86-64.so.2, for GNU/Linux 2.6.32, with debug_info, not stripped

$ ./build/bin/hello
Hello, world!

Note, however, that currently there are no formal guarantees about the code generation.

$\endgroup$
1
  • $\begingroup$ I would add bum.pm as alternative build tool and package manager for Lean 4 :-) $\endgroup$ Feb 8, 2022 at 23:38
4
$\begingroup$

HOL4 + CakeML support generation of verified machine code guaranteed to be equivalent to the semantics of the input program. There are techniques for

  • verifying the input program at the level of functional programming, and
  • generating input programs from the language of HOL functions (about which one might have separately proved properties of interest).
$\endgroup$
2
$\begingroup$

Depending on your particular needs, it may also be an option to write your programs in a general purpose programming language first, and then import it into your theorem proving environment to reason about it, e.g. using tools like hs-to-coq.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.