Merge pull request #20 from tmattio/success-stories

Add success stories

Makefile

@@ -0,0 +1,54 @@
+.DEFAULT_GOAL := all
+
+ARGS := $(wordlist 2,$(words $(MAKECMDGOALS)),$(MAKECMDGOALS))
+$(eval $(ARGS):;@:)
+
+.PHONY: all
+all:
+	opam exec -- dune build --root . @install
+
+.PHONY: dev
+dev: ## Install development dependencies
+	opam switch create . --no-install -y
+	opam install -y dune-release ocamlformat utop ocaml-lsp-server
+	opam install --deps-only --with-test --with-doc -y .
+
+.PHONY: build
+build: ## Build the project, including non installable libraries and executables
+	opam exec -- dune build --root .
+
+.PHONY: start
+start: all ## Start the project
+	opam exec -- dune exec --root . src/bin/main.exe $(ARGS)
+
+.PHONY: install
+install: all ## Install the packages on the system
+	opam exec -- dune install --root .
+
+.PHONY: test
+test: ## Run the unit tests
+	opam exec -- dune runtest --root .
+
+.PHONY: clean
+clean: ## Clean build artifacts and other generated files
+	opam exec -- dune clean --root .
+
+.PHONY: doc
+doc: ## Generate odoc documentation
+	opam exec -- dune build --root . @doc
+
+.PHONY: servedoc
+servedoc: doc ## Open odoc documentation with default web browser
+	open _build/default/_doc/_html/index.html
+
+.PHONY: fmt
+fmt: ## Format the codebase with ocamlformat
+	opam exec -- dune build --root . @fmt --auto-promote
+
+.PHONY: watch
+watch: ## Watch for the filesystem and rebuild on every change
+	opam exec -- dune build --root . --watch
+
+.PHONY: utop
+utop: ## Run a REPL and link with the project's libraries
+	opam exec -- dune utop --root . lib -- -implicit-bindings

data/success_stories/en/astree.md

@@ -0,0 +1,34 @@
+---
+title: The ASTRÉE Static Analyzer
+image: astree-thumb.gif
+url: http://www.astree.ens.fr/
+---
+
+*[David Monniaux](http://www-verimag.imag.fr/~monniaux/) (CNRS), member
+of the ASTRÉE project, says:* “[ASTRÉE](http://www.astree.ens.fr/) is a
+*static analyzer* based on *[abstract
+interpretation](http://www.di.ens.fr/%7Ecousot/aiintro.shtml)* 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](https://www.airbus.com/aircraft/previous-generation-aircraft/a340-family.html). 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](http://www.astree.ens.fr/) is written in OCaml 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.”

data/success_stories/en/coq.md

@@ -0,0 +1,23 @@
+---
+title: Coq
+image: coq-thumb.jpg
+url: http://coq.inria.fr/
+---
+
+*[Jean-Christophe Filliâtre](https://www.lri.fr/~filliatr/) (CNRS), a
+Coq developer, says:* “The [Coq](http://coq.inria.fr/) 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, OCaml is attractive on multiple grounds.
+First, the OCaml language is perfectly suited for symbolic
+manipulations, which are of paramount importance in a proof assistant.
+Furthermore, OCaml'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,
+OCaml'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.”

data/success_stories/en/fftw.md

@@ -0,0 +1,20 @@
+---
+title: FFTW
+image: fftw-thumb.png
+url: http://www.fftw.org/
+---
+
+[FFTW](http://www.fftw.org/) is a [very fast](http://www.fftw.org/benchfft/) 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](https://en.wikipedia.org/wiki/J._H._Wilkinson_Prize_for_Numerical_Software)
+for numerical software.
+
+Benchmarks, performed 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.”

data/success_stories/en/haxe.md

@@ -0,0 +1,9 @@
+---
+title: Haxe
+url: http://haxe.org/
+---
+
+[Haxe](http://haxe.org/) is an open source toolkit based on a modern,
+high level, strictly typed programming language, a cross-compiler,
+a complete cross-platform standard library and ways to access each
+platform's native capabilities. The Haxe compiler was entirely written in OCaml.

data/success_stories/en/jane_street.md

@@ -0,0 +1,27 @@
+---
+title: Jane Street
+image: jane-street-thumb.jpg
+url: http://janestreet.com/technology/
+---
+
+Jane Street is a proprietary trading firm that uses OCaml as its primary
+development platform.  Our operation runs at a large scale,
+generating billions of dollars of transactions every day from our offices
+in Hong Kong, London and New York, with strategies that span many asset classes,
+time-zones and regulatory regimes.
+
+Almost all of our software is written in OCaml, from statistical
+research code to systems-administration tools to our real-time trading
+infrastructure.  OCaml’s type system acts as a rich and
+well-integrated set of static analysis tools that help improve the
+quality of our code, catching bugs at the earliest possible stage.
+Billions of dollars of transactions flow through our systems every day,
+so getting it right matters.  At the same time, OCaml is highly productive,
+helping us quickly adapt to changing market conditions.
+
+Jane Street has been contributing open-source libraries back to the wider
+community for many years, including Core, our alternative standard
+library, Async, a cooperative concurrency library,
+and several syntax extensions like binprot and sexplib.  All of these can
+be found at [http://janestreet.github.io](http://janestreet.github.io).  All in, we've open-sourced
+more than 200k lines of code.

data/success_stories/en/lexifi.md

@@ -0,0 +1,35 @@
+---
+title: LexiFi's Modeling Language for Finance
+image: lexifi-thumb.jpg
+url: http://www.lexifi.com/
+---
+
+Developed by the company [LexiFi](http://www.lexifi.com/), 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.

data/success_stories/en/liquidsoap.md

@@ -0,0 +1,10 @@
+---
+title: Liquidsoap
+---
+
+[Liquidsoap](https://www.liquidsoap.info/) is clearly well established in the
+(internet) radio industry. Liquidsoap is well known as a tool with
+unique abilities, and has lots of users including big commercial ones.
+It is not developed as a business, but companies develop services or
+software on top of it. For example, Sourcefabric develops and sells
+Airtime on top of Liquidsoap.

data/success_stories/en/mldonkey.md

@@ -0,0 +1,25 @@
+---
+title: The MLdonkey peer-to-peer client
+image: mldonkey-thumb.jpg
+url: http://mldonkey.sourceforge.net/Main_Page
+---
+
+[MLdonkey](http://mldonkey.sourceforge.net/Main_Page) 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 OCaml 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 [free(code)](http://freecode.com/) (formerly “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.”

data/success_stories/en/slam.md

@@ -0,0 +1,22 @@
+---
+title: SLAM
+url: http://research.microsoft.com/en-us/projects/slam/
+---
+
+The [SLAM](http://research.microsoft.com/en-us/projects/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](http://research.microsoft.com/apps/pubs/default.aspx?id=70038),
+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.”

data/success_stories/en/unison.md

@@ -0,0 +1,30 @@
+---
+title: The Unison File Synchronizer
+image: unison-thumb.jpg
+url: http://www.cis.upenn.edu/%7Ebcpierce/unison/
+---
+
+[Unison](http://www.cis.upenn.edu/%7Ebcpierce/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](http://www.cis.upenn.edu/%7Ebcpierce/) (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.”

data/success_stories/fr/astree.md

@@ -0,0 +1,38 @@
+---
+title: L'analyseur statique ASTRÉE
+image: astree-thumb.gif
+url: http://www.astree.ens.fr/
+---
+
+*[David Monniaux](http://www-verimag.imag.fr/~monniaux/) (CNRS), membre
+du projet ASTRÉE :* « [ASTRÉE](http://www.astree.ens.fr/) est un
+*analyseur statique* basé sur [l'interprétation
+abstraite](http://www.di.ens.fr/%7Ecousot/aiintro.shtml) et qui vise à
+établir l'absence d'erreurs d'exécution dans des logiciels critiques
+écrits dans un sous-ensemble du langage C. »
+
+« Une analyse automatique et exacte visant à vérifier des propriétés
+telles que l'absence d'erreurs d'exécution est impossible en général,
+pour des raisons mathématiques. L'analyse statique par interprétation
+abstraite contourne cette impossibilité, et permet de prouver des
+propriétés de programmes, en sur-estimant l'ensemble des comportements
+possibles d'un programme. Il est possible de concevoir des
+approximations pessimistes qui, en pratique, permettent d'établir la
+propriété souhaitée pour une large gamme de logiciels. »
+
+« À ce jour, ASTRÉE a prouvé l'absence d'erreurs d'exécution dans le
+logiciel de contrôle primaire de la [famille Airbus
+A340](http://www.airbus.com/product/a330_a340_backgrounder.asp). Cela
+serait impossible par de simples *tests*, car le test ne considère qu'un
+*sous-ensemble* limité des cas, tandis que l'interprétation abstraite
+considère un *sur-ensemble* de tous les comportements possibles du
+système. »
+
+« [ASTRÉE](http://www.astree.ens.fr/) est écrit en OCaml et mesure
+environ 44000 lignes (plus des librairies externes). Nous avions besoin
+d'un langage doté d'une bonne performance (en termes de vitesse et
+d'occupation mémoire) sur un matériel raisonnable, favorisant l'emploi
+de structures de données avancées, et garantissant la sûreté mémoire.
+OCaml permet également d'organiser le code source de façon modulaire,
+claire et compacte, et facilite la gestion de structures de données
+récursives comme les arbres de syntaxe abstraite. »

data/success_stories/fr/coq.md

@@ -0,0 +1,23 @@
+---
+title: Coq
+image: coq-thumb.jpg
+url: http://coq.inria.fr/
+---
+
+*[Jean-Christophe Filliâtre](http://www.lri.fr/%7Efilliatr/) (CNRS), un
+des développeurs de Coq :* « L'outil [Coq](http://coq.inria.fr/) est un
+système de manipulation de preuves mathématiques formelles ; une preuve
+réalisée avec Coq est mécaniquement vérifiée par la machine. Outre ses
+applications en mathématiques, l'outil Coq permet également de certifier
+la correction de programmes informatiques. »
+
+« L'intérêt de OCaml du point de vue de Coq est multiple. D'une part, le
+langage OCaml est parfaitement adapté aux manipulations symboliques, qui
+sont prépondérantes dans un assistant de preuve. D'autre part, le
+système de types de OCaml, et notamment sa notion de type abstrait,
+permet une réelle encapsulation de la partie critique du code de Coq,
+garantissant ainsi la cohérence logique de l'ensemble du système. Enfin,
+le typage fort de OCaml assure de fait une grande qualité au code de Coq
+(tel que l'absence d'erreurs à l'exécution du type « segmentation
+fault »), ce qui est indispensable à un outil dont le but premier est
+justement la rigueur. »

data/success_stories/fr/ensemble.md

@@ -0,0 +1,22 @@
+---
+title: Le système de communication distribuée Ensemble
+url: http://dsl.cs.technion.ac.il/projects/Ensemble/
+---
+
+*Ohad Rodeh (IBM Haifa), un des développeurs d'Ensemble :*
+« [Ensemble](http://dsl.cs.technion.ac.il/projects/Ensemble/) est un
+système de communication de groupe écrit en OCaml, développé à Cornell
+et à Hebrew University. À l'auteur d'applications, Ensemble fournit une
+librairie de protocoles que l'on peut utiliser pour construire
+rapidement des applications distribuées complexes. Pour un chercheur en
+systèmes distribués, Ensemble est une boîte à outils hautement modulaire
+et reconfigurable : les protocoles de haut niveau fournis aux
+applications sont en réalité des piles de minuscules « couches » de
+protocoles, dont chacune peut être modifiée ou reconstruite à des fins
+d'expérimentation. OCaml a été choisi initialement pour que le code
+puisse être vérifié par un prouveur de théorèmes semi-automatique. Ce
+code a ensuite fait ses preuves sur le terrain, et nous avons continué à
+développer en OCaml. Le système de types fort, les types de données
+algébriques, la récupération automatique de la mémoire et
+l'environnement d'exécution sont les principales raisons de notre
+intérêt pour OCaml. »