btw: Lean 4 is getting all the buzz these days, but how many people know that Scheme/Racket is an extraction target language for the Rocq Prover (aka Coq).
The Rocq Prover implements a high-level program specification and mathematical language called Gallina that is based on an expressive formal language called the Polymorphic, Cumulative Calculus of Inductive Constructions that itself combines both a higher-order logic and a richly-typed functional programming language. Through a vernacular language of commands, the Rocq Prover allows:
to define data structures, functions or predicates, that can be evaluated efficiently;
to state mathematical theorems and software specifications;
to interactively develop formal proofs of these theorems;
to machine-check these proofs by a relatively small certification "kernel";
to extract certified programs to languages like OCaml, Haskell or Scheme.
As a proof development system, the Rocq Prover provides interactive proof methods, decision and semi-decision algorithms, and a tactic language for letting the user define its own proof methods. Connection with external computer algebra systems or theorem provers is available.
As a platform for the formalization of mathematics or the development of programs, the Rocq Prover provides support for high-level notations, implicit contents and other mechanisms for formalization at scale.
https://rocq-prover.org/
The Rocq Prover implements a high-level program specification and mathematical language called Gallina that is based on an expressive formal language called the Polymorphic, Cumulative Calculus of Inductive Constructions that itself combines both a higher-order logic and a richly-typed functional programming language. Through a vernacular language of commands, the Rocq Prover allows:
As a proof development system, the Rocq Prover provides interactive proof methods, decision and semi-decision algorithms, and a tactic language for letting the user define its own proof methods. Connection with external computer algebra systems or theorem provers is available.As a platform for the formalization of mathematics or the development of programs, the Rocq Prover provides support for high-level notations, implicit contents and other mechanisms for formalization at scale.