Is there a informatic theory behind ocaml

Learning
1

When ocaml was developed, was there a “theory” used ?
Or it was just developed as needed.
I found this link,
https://coq.inria.fr/
If i’m correct some mathematical statements can be proven true if you can write a “just” program.
Feel free to elaborate (please using not too complicated language)

2

Caml (the predecessor of OCaml) was based on the “Categorical Abstract Machine” Categorical abstract machine - Wikipedia. See A History of Caml for more.

Cheers,
Nicolas

5 Likes
3

In general, functional languages are based on the Lambda Calculus.

1 Like
4

Regarding the safety properties enjoyed by OCaml programs, this is mostly related to type system research. The main practical takeaway is that well-typed programs do not crash. If you’re interested in the precise formulation of this results and the theory behind it, B. C. Pierce’s Types and Programming Languages is a good reference. The examples use an ML-like language, so very close to OCaml.

1 Like
5

Perhaps start with Xavier Leroy’s Master’s thesis (D.E.A. in French, IIRC) and follow citation links forward and backward. It’s an excellent thesis, BTW.

1 Like
6

OCaml was based on CAML, which was based on ML. CAML was evidently a bacronym for “Categorical Abstract Machine Language”, but ML was an originally an acronym for “Meta Language”. That’s because it originated in Robin Milner’s “Logic for Computable Functions” (LCF), first at Stanford, then at Edinburgh - emphasis on “Logic”. It was designed as the Meta Language for a proof system. Which means it was based not on the Lambda Calculus but the Sequent Calculus, some version of which is the most commonly used calculus in Logic and Proof Theory. The Lambda Calculus plays a major role in ML, though, since by the Curry-Howard isomorphism logic and computation are two sides of the same coin - implication (logic) corresponding to function (computation). I believe the major innovation of ML was its type inferencing capabilities, which are used in some form by most strongly typed languages today.

In short, yes, there’s tons of fascinating theory behind OCaml. There’s a reason it is so popular in the world of automated verification.

For more on ML see Edinburgh LCF. The documentation for NuPrl also covers ML. OCaml of course adds a bunch of stuff.

HTH,

Gregg

6 Likes