smorimoto/coq-to-ocaml-to-js

---

smorimoto/coq-to-ocaml-to-js.json

{
  "createdAt": "2019-10-24T03:24:02Z",
  "defaultBranch": "master",
  "description": "Proof of concept to generate safe and fast JavaScript",
  "fullName": "smorimoto/coq-to-ocaml-to-js",
  "homepage": "",
  "language": "JavaScript",
  "name": "coq-to-ocaml-to-js",
  "pushedAt": "2022-08-07T15:30:42Z",
  "stargazersCount": 24,
  "topics": [
    "bucklescript",
    "coq",
    "javascript",
    "ocaml",
    "proof"
  ],
  "updatedAt": "2024-12-11T19:59:24Z",
  "url": "https://github.com/smorimoto/coq-to-ocaml-to-js"
}

coq-to-ocaml-to-js

Overview

This repository is nothing more than a proof of concept using Coq’s Extraction, BuckleScript, Rollup, Terser, and Closure Compiler to generate safe and fast JavaScript.

What is Coq

Coq is a proof assistant. It means that it is designed to develop mathematical proofs, and especially to write formal specifications, programs and proofs that programs comply to their specifications. An interesting additional feature of Coq is that it can automatically extract executable programs from specifications, as either Objective Caml or Haskell source code. - A short introduction to Coq

What is BuckleScript

BuckleScript isn’t a new language. It simply takes OCaml, a fast, pragmatic and typed language, and makes it compile to clean, readable and performant JavaScript code. - What is BuckleScript?

Workflow and directory structure

Coq Code
  |
  | (Use Coq Compiler)
  v
OCaml Code
  |
  | (Use BuckleScript)
  v
Optimized JavaScript Code
  |
  | (Use Rollup, Terser, Closure Compiler)
  v
More Optimized JavaScript Code

Source code

Fixpoint f n :=
  match n with
  | O => nat
  | S n => nat -> (f n)
  end.

Definition sigma: forall n, f n.
  intro n; induction n; simpl.
    exact O.
  intro m.
  destruct n; simpl in *.
    exact m.
  intro o.
  apply IHn.
  exact (m+o).
Defined.

Generated codes

sigma.ml

type __ = Obj.t
type nat = O | S of nat

(** val add : nat -> nat -> nat **)

let rec add n m = match n with O -> m | S p -> S (add p m)

type f = __

(** val sigma : nat -> f **)

let rec sigma = function
  | O -> Obj.magic O
  | S n0 ->
      Obj.magic (fun m ->
          match n0 with
          | O -> m
          | S _ -> fun o -> Obj.magic sigma n0 (add (Obj.magic m) o))

sigma.mli

type __ = Obj.t
type nat = O | S of nat

val add : nat -> nat -> nat

type f = __

val sigma : nat -> f

sigma.js

import * as Curry from "rescript/lib/es6/curry.js";

function add(n, m) {
  if (n) {
    return /* S */ {
      _0: add(n._0, m),
    };
  } else {
    return m;
  }
}

function sigma(n0) {
  if (!n0) {
    return /* O */ 0;
  }
  var n0$1 = n0._0;
  return function (m) {
    if (n0$1) {
      return function (o) {
        return Curry._1(sigma(n0$1), add(m, o));
      };
    } else {
      return m;
    }
  };
}

export { add, sigma };

Build

See the file [BUILD.md]!(BUILD.md) for build instructions.

License

Licensed under the Apache License, Version 2.0.