# Formal Verification for OCaml

**URL:** <https://discuss.ocaml.org/t/formal-verification-for-ocaml/7954>\
**Category:** Learning\
**Created:** [June 2, 2021, 10:32am UTC](https://discuss.ocaml.org/t/formal-verification-for-ocaml/7954 "2021-06-02T10:32:04Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![DonCorleone](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/doncorleone/32/2985_2.png) [@DonCorleone](https://discuss.ocaml.org/u/DonCorleone)\
**Post date:** [June 2, 2021, 10:32am UTC](https://discuss.ocaml.org/t/formal-verification-for-ocaml/7954/1 "2021-06-02T10:32:04Z")

</div>

let rec map = fun f l →   
match l with [] → [] | x::xs → f x :: map f xs  
and fold\_left = fun f a l →   
match l with [] → a | x::xs → fold\_left f (f a x) xs  
and comp = fun f g x → f (g x)  
and mul = fun a b → a \* b  
and id = fun x → x the task is to prove fold\_left mul 3 [10] ⇒ 30

---

<div class="post-metadata">

**Author:** ![bcc32](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/bcc32/32/203_2.png) [@bcc32](https://discuss.ocaml.org/u/bcc32)\
**Post date:** [June 2, 2021, 2:32pm UTC](https://discuss.ocaml.org/t/formal-verification-for-ocaml/7954/2 "2021-06-02T14:32:24Z")

</div>

Hi @DonCorleone, is this a homework question? We [do not permit](https://discuss.ocaml.org/t/should-we-be-answering-peoples-homeworks/2123) this forum to be used for simply exchanging homework solutions, although if you have specific questions about something you do not understand in OCaml or formal verification, you are free to ask those.

---

<div class="post-metadata">

**Author:** ![cloudyhug](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/cloudyhug/32/2399_2.png) [@cloudyhug](https://discuss.ocaml.org/u/cloudyhug)\
**Post date:** [June 2, 2021, 7:49pm UTC](https://discuss.ocaml.org/t/formal-verification-for-ocaml/7954/3 "2021-06-02T19:49:28Z")

</div>

Hello. I am not sure what you exactly need because you did not really explain it clearly.

A formal verification approach could use a proof assistant like Coq, whose programming language, Gallina, is an advanced version of OCaml with dependent types and a specific relation to logic called the Curry-Howard isomorphism. However, it is clearly overkill on this kind of example because the proof you are asking for can be done just by computing the left hand term (`reflexivity`).

Maybe you were asked to give details about the reduction in OCaml that leads to this result?

```coq
From Coq Require Import List.
Import ListNotations.

Fixpoint map {A B : Type} (f : A -> B) (l : list A) : list B :=
  match l with
  | [] => []
  | x :: xs => f x :: map f xs
  end.

Fixpoint fold_left {A B : Type} (f : A -> B -> A) (a : A) (l : list B) : A :=
  match l with
  | [] => a
  | x :: xs => fold_left f (f a x) xs
  end.

Definition mul (a b : nat) : nat := a * b.

Goal fold_left mul 3 [10] = 30.
Proof. reflexivity. Qed.

```

The advantage of a proof assistant is that you could prove for example that the product of a list containing 0 is always 0. This is a more general results than your computation and Coq allows to reason about that.

---

<div class="post-metadata">

**Author:** ![DonCorleone](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/doncorleone/32/2985_2.png) [@DonCorleone](https://discuss.ocaml.org/u/DonCorleone)\
**Post date:** [June 25, 2021, 8:53am UTC](https://discuss.ocaml.org/t/formal-verification-for-ocaml/7954/4 "2021-06-25T08:53:12Z")

</div>

exactly, I wanted such proof… thank you.