Proof Assistants with support for creating executable software artifacts

Question

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.

Answer 1

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.

Answer 2

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.

Answer 3

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

Answer 4

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.