Unison is a popular file-synchronization tool for Windows and most flavors of Unix. It allows two replicas of a collection of files and directories to be stored on different hosts (or different disks on the same host), modified separately, and then brought up to date by propagating the changes in each replica to the other. Unlike simple mirroring or backup utilities, Unison can deal with updates to both replicas: updates that do not conflict are propagated automatically and conflicting updates are detected and displayed. Unison is also resilient to failure: it is careful to leave the replicas and its own private structures in a sensible state at all times, even in case of abnormal termination or communication failures.

Benjamin C. Pierce (University of Pennsylvania), Unison project leader, says: “I think Unison is a very clear success for OCaml – in particular, for the extreme portability and overall excellent engineering of the compiler and runtime system. OCaml's strong static typing, in combination with its powerful module system, helped us organize a large and intricate codebase with a high degree of encapsulation. This has allowed us to maintain a high level of robustness through years of work by many different programmers. In fact, Unison may be unique among large OCaml projects in having been translated from Java to OCaml midway through its development. Moving to OCaml was like a breath of fresh air.”

MLdonkey is a multi-platform multi-networks peer-to-peer client. It was the first open-source client to access the eDonkey network. Today, MLdonkey supports several other large networks, among which Overnet, Bittorrent, Gnutella, Gnutella2, Fasttrack, Soulseek, Direct-Connect, and Opennap. Searches can be conducted over several networks concurrently; files are downloaded from and uploaded to multiple peers concurrently.

An MLdonkey developer says: “Early in 2002, we decided to use Objective Caml to program a network application in the emerging world of peer-to-peer systems. The result of our work, MLdonkey, has surpassed our hopes: MLdonkey is currently the most popular peer-to-peer file-sharing client according to freshmeat.net, with about 10,000 daily users. Moreover, MLdonkey is the only client able to connect to several peer-to-peer networks, to download and share files. It works as a daemon, running unattended on the computer, and can be controlled remotely using a choice of three different kinds of interfaces: GTK, web and telnet.”

Developed by the company LexiFi, the Modeling Language for Finance (MLFi) is the first formal language that accurately describes the most sophisticated capital market, credit, and investment products. MLFi is implemented as an extension of OCaml.

MLFi users derive two important benefits from a functional programming approach. First, the declarative formalism of functional programming languages is well suited for specifying complex data structures and algorithms. Second, functional programming languages have strong list processing capabilities. Lists play a central role in finance where they are used extensively to define contract event and payment schedules.

In addition, MLFi provides crucial business integration capabilities inherited from OCaml and related tools and libraries. This enables users, for example, to interoperate with C and Java programs, manipulate XML schemas and documents, and interface with SQL databases.

Data models and object models aiming to encapsulate the definitions and behavior of financial instruments were developed by the banking industry over the past two decades, but face inherent limitations that OCaml helped overcome.

LexiFi's approach to modeling complex financial contracts received an academic award in 2000, and the MLFi implementation was elected “Software Product of the Year 2001” by the magazine Risk, the leading financial trading and risk management publication. MLFi-based solutions are gaining growing acceptance throughout Europe and are contributing to spread the use of OCaml in the financial services industry.

Ohad Rodeh (IBM Haifa), an Ensemble developer, says: “Ensemble is a group communication system written in the OCaml programming language, developed at Cornell and the Hebrew University. For an application builder, Ensemble provides a library of protocols that can be used for quickly building complex distributed applications. For a distributed systems researcher, Ensemble is a highly modular and reconfigurable toolkit: the high-level protocols provided to applications are really stacks of tiny protocol “layers”, each of whose can be modified or rebuilt to experiment. OCaml was initially chosen so that the code could be proven by a semi-automatic theorem prover. The code proved itself in the field later on, and we continued to develop in OCaml. The strong type system, algebraic data types, automatic garbage collection, and good run-time system are the main reasons we like OCaml.”

Jean-Christophe Filliâtre (CNRS), a Coq developer, says: “The Coq tool is a system for manipulating formal mathematical proofs; a proof carried out in Coq is mechanically verified by the machine. In addition to its applications in mathematics, Coq also allows certifying the correctness of computer programs.”

“From the Coq standpoint, Caml is attractive on multiple grounds. First, the Caml language is perfectly suited for symbolic manipulations, which are of paramount importance in a proof assistant. Furthermore, Caml's type system, and particularly its notion of abstract type, allow securely encapsulating Coq's critical code base, which guarantees the logical consistency of the whole system. Last, Caml's strong type system de facto grants Coq's code a high level of quality: errors such as “segmentation faults” cannot occur during execution, which is indispensable for a tool whose primary goal is precisely rigor.”

David Monniaux (CNRS), member of the ASTRÉE project, says: “ASTRÉE is a static analyzer based on abstract interpretation that aims at proving the absence of runtime errors in safety-critical software written in a subset of the C programming language.”

“Automatically analyzing programs for exactly checking properties such as the absence of runtime errors is impossible in general, for mathematical reasons. Static analysis by abstract interpretation works around this impossibility and proves program properties by over-approximating the possible behaviors of the program: it is possible to design pessimistic approximations that, in practice, allow proving the desired property on a wide range of software.”

“So far, ASTRÉE has proved the absence of runtime errors in the primary control software of the Airbus A340 family. This would be impossible by software testing, for testing only considers a limited subset of the test cases, while abstract interpretation considers a superset of all possible outcomes of the system.”

“ASTRÉE is written in Objective Caml and is about 44000 lines long (plus external libraries). We needed a language with good performance (speed and memory usage) on reasonable equipment, easy support for advanced data structures, and type and memory safety. OCaml also allows for modular, clear and compact source code and makes it easy to work with recursive structures such as syntax trees.”

The SLAM project originated in Microsoft Research in early 2000. Its goal was to automatically check that a C program correctly uses the interface to an external library. The project used and extended ideas from symbolic model checking, program analysis and theorem proving in novel ways to address this problem. The SLAM analysis engine forms the core of a new tool called Static Driver Verifier (SDV) that systematically analyzes the source code of Windows device drivers against a set of rules that define what it means for a device driver to properly interact with the Windows operating system kernel.

In technical report MSR-TR-2004-08, T.Ball, B.Cook, V.Levin and S.K.Rajamani, the SLAM developers, write: “The Right Tools for the Job: We developed SLAM using INRIA's OCaml functional programming language. The expressiveness of this language and robustness of its implementation provided a great productivity boost.”

FFTW is a very fast C library for computing Discrete Fourier Transforms (DFT). It uses a powerful symbolic optimizer written in OCaml which, given an integer N, generates highly optimized C code to compute DFTs of size N. FFTW was awarded the 1999 Wilkinson prize for numerical software.

Benchmarks, performed on on a variety of platforms, show that FFTW's performance is typically superior to that of other publicly available DFT software, and is even competitive with vendor-tuned codes. In contrast to vendor-tuned codes, however, FFTW's performance is portable: the same program will perform well on most architectures without modification. Hence the name, “FFTW,” which stands for the somewhat whimsical title of “Fastest Fourier Transform in the West.”