• en

# OCaml Planet

The OCaml Planet aggregates various blogs from the OCaml community. If you would like to be added, read the Planet syndication HOWTO.

929 blog posts are available. You can read the 30 more recent ones below or view older ones.

# Intermediate truth values — Andrej Bauer, Jul 30, 2015

I have not written a blog post in a while, so I decided to write up a short observation about truth values in intuitionistic logic which sometimes seems a bit puzzling.

Let $\Omega$ be the set of truth values (in Coq this would be the setoid whose underlying type is $\mathsf{Prop}$ and equality is equivalence $\leftrightarrow$, while in HoTT it is the h-propostions). Call a truth value $p : \Omega$ intermediate if it is neither true nor false, i.e., $p \neq \bot$ and $p \neq \top$. Such a R…

# Formally verifying the complexity of OCaml programs with CFML -- interlude — GaGallium (Armaël Guéneau), Jul 30, 2015

This small interlude post is not about Coq nor CFML: I present a data structure from Okasaki's Purely functional data structures, implemented in OCaml.

It comes as a preliminary explanation for an incoming formalization of it in CFML, including an complexity analysis!

The structure we decided to study is Okasaki's "binary random access list". It is a functional data structure, which features usual list operations (cons and uncons for adding and removing an element at the h…

# Fun With Opam: Advice to My Past Self — Mindy Preston, Jul 27, 2015

Most instructions on how to get started with OCaml packages now advise the user to get started with opam, which is excellent advice. Getting up and running with opam is pretty easy, but I wasn’t sure where to go from there when I wanted to modify other people’s packages and use the modifications in my environment. I wish I’d realized that the documentation for making packages has a lot of applicable advice for that use case, as well as the apparent target (making your own packges from scra…

# Organized chaos: managing randomness — Open Mirage (David Kaloper), Jul 22, 2015

This post gives a bit of background on the Random Number Generator (RNG) in the recent MirageOS v2.5 release.

First we give background about why RNGs are really critical for security. Then we try to clarify the often-confused concepts of "randomness" and "entropy", as used in this context. Finally, we explore the challenges of harvesting good-quality entropy in a unikernel environment.

### Playing dice

Security software must play dice.

It must do so to create secrets, for…

# Full Time: Sr. Software Engineer-Java Scala at The Weather Channel in Atlanta, GA — GitHub Jobs, Jul 21, 2015

The Weather Channel has two 6-month contracting and five full-time openings!

Our Java Development team is seeking a passionate programmer who is excited about the opportunity to use Scala and functional programming techniques in professional software development environment. Key responsibilities in this position include design, implementation, testing, and deployment of sophisticated backend software systems using Scala, Java, and Clojure. The incumbent will be part of a motivated team of dev…

# Building the LLVM Fuzzer on Debian. — Erik de Castro Lopo, Jul 21, 2015

I've been using the awesome American Fuzzy Lop fuzzer since late last year but had also heard good things about the LLVM Fuzzer. Getting the code for the LLVM Fuzzer is trivial, but when I tried to use it, I ran into all sorts of road blocks.

Firstly, the LLVM Fuzzer needs to be compiled with and used with Clang (GNU GCC won't work) and it needs to be Clang >= 3.7. Now Debian does ship a clang-3.7 in the Testing and Unstable releases, but that package has a bug (#779785) which means the…

# OCaml server-side developer at Ahrefs Research (Full-time) — Functional Jobs (FunctionalJobs.com), Jul 20, 2015

## Who we are

Ahrefs Research is a San Francisco branch of Ahrefs Pte Ltd (Singapore), which runs an internet-scale bot that crawls whole Web 24/7, storing huge volumes of information to be indexed and structured in timely fashion. On top of that Ahrefs is building analytical services for end-users.

Ahrefs Research develops a custom petabyte-scale distributed storage to accommodate all that data coming in at high speed, focusing on performance, robustness and ease of use. Performance-critical low…

# Introducing Incremental — Jane Street (Yaron Minsky), Jul 18, 2015

I'm pleased to announce the release of Incremental (well commented mli here), a powerful library for building self-adjusting computations, i.e., computations that can be updated efficiently when their inputs change.

At its simplest, you can think of a self-adjusting computation as a fancy spreadsheet. In a spreadsheet, each cell contains either simple data, or an equation that describes how the value in this cell should be derived from values in other cells. Collectively, this amounts to a graph…

# Formally verifying the complexity of OCaml programs with CFML -- part 1 — GaGallium (Armaël Guéneau), Jul 18, 2015

In a recent paper, Arthur Charguéraud and François Pottier present a formal proof of an OCaml implementation of Tarjan's union-find algorithm. The proof covers two aspects: first, functional correctness ("the algorithm is correct"), but also asymptotic complexity. For example, one of the results of the paper is that the link function runs in $$O(α(n))$$ elementary steps, $$α$$ being the inverse of the Ackermann function.

Actually, the complexity results of the paper are no…

# ocaml-fileutils 0.5.0 released — OCamlCore Forge News ( (Sylvain Le Gall), Jul 13, 2015

A new version of ocaml-fileutils has been published. OCaml Fileutils provides functions to manipulate files (like rm, cp, touch, find, mv, which) and filenames. The library is pure OCaml and as much as possible portable. The release: https://forge.ocamlcore.org/frs/shownotes.php?release_id=1154 More information: http://ocaml-fileutils.forge.ocamlcore.org/

# Converting a code base from camlp4 to ppx — Jane Street (Jeremie Dimino), Jul 08, 2015

As with many projects in the OCaml world, at Jane Street we have been working on migrating from camlp4 to ppx. After having developed equivalent ppx rewriters for our camlp4 syntax extensions, the last step is to actually translate the code source of all our libraries and applications from the camlp4 syntax to the standard OCaml syntax with extension points and attributes.

For instance to translate code using pa_ounit and pa_test, we have to rewrite:

TEST = <:test_result< int >> ~exp…

# Unikernels: HTTP -> HTTPS

Building a static website is one of the better-supported user stories for MirageOS, but it currently results in an HTTP-only site, with no capability for TLS. Although there's been a great TLS stack available for a while now, it was a bit fiddly to assemble the pieces of TLS, Cohttp, and the MirageOS frontend tool in order to construct an HTTPS unikernel. With MirageOS 2.5, that's changed! Let's celebrate by building an HTTPS-serving unikernel of our very …

# Unikernels at PolyConf! — Amir Chaudhry, Jul 04, 2015

Updated: 14 July (see below)

Above are my slides from a talk at PolyConf this year. I was originally going to talk about the MISO tool stack and personal clouds (i.e. how we’ll build towards Nymote) but after some informal conversations with other speakers and attendees, I thought it would be way more useful to focus the talk on unikernels themselves — specifically, the ‘M’ in MISO. As a result, I ended up completely rewriting all my slides! Since I pushed this post just before my…

# Reviewing the Bitcoin Pinata — Open Mirage (Hannes Mehnert), Jun 29, 2015

TL;DR: Nobody took our BTC. Random people from the Internet even donated into our BTC wallet. We showed the feasibility of a transparent self-service bounty. In the style of Dijkstra: security bounties can be a very effective way to show the presence of vulnerabilities, but they are hopelessly inadequate for showing their absence.

#### What are you talking about?

Earlier this year, we released a Bitcoin Piñata. The Piñata was a security bounty containing 10 BTC and it's been online since …

# MirageOS v2.5 with full TLS support — Open Mirage (Amir Chaudhry), Jun 26, 2015

Today we're announcing the new release of MirageOS v2.5, which includes first-class support for SSL/TLS in the MirageOS configuration language. We introduced the pure OCaml implementation of transport layer security (TLS) last summer and have been working since then to improve the integration and create a robust framework. The recent releases allow developers to easily build and deploy secure unikernel services and we've also incorporated numerous bug-fixes and major stability improvemen…

# Why OCaml-TLS? — Open Mirage (Amir Chaudhry), Jun 26, 2015

TLS implementations have a history of security flaws, which are often the result of implementation errors. These security flaws stem from the underlying challenges of interpreting ambiguous specifications, the complexities of large APIs and code bases, and the use of unsafe programming practices.

Re-engineering security-critical software allows the opportunity to use modern approaches to prevent these recurring issues. Creating the TLS stack in OCaml offers a range of benefits, including…

# Cumulative moving average — Shayne Fletcher, Jun 25, 2015

We have $nA_{N} = s_{1} + \cdots + s_{n}$ and $(n + 1)A_{n + 1} = s_{1} + \cdots + s_{n + 1}$ so $s_{n + 1} = (n + 1)A_{n + 1} - nA_{n}$ from which we observe $A_{n + 1} = \frac{s_{n + 1} + nA_{n}}{n + 1} = A_{n} + \frac{s_{n + 1} + nA_{n}}{n + 1} - A_{n} = A_{n} + \frac{s_{n + 1} - A_{n}}{n + 1}$.

OCaml:

let cumulative_moving_average (l : float list) : float =  let f (s, i) x =    let k = i + 1 in    let s = (s +. (x -. s)/. (float_of_int k)) in    (s, k) in  fst @@ List.fold_left f (0., 0) l

Fe…

# Using Coq's evaluation mechanisms in anger — GaGallium (Xavier Leroy), Jun 23, 2015

Coq offers several internal evaluation mechanisms that have many uses, from glorious proofs by reflection to mundane testing of functions. Read on for an account of my quest to get large parts of the CompCert verified C compiler to execute from within Coq. It was a mighty battle between the forces of transparency and opacity, with the innocent-looking "decide equality" tactic as the surprise villain...

Recently, I spent significant time trying to execute parts of the CompCert ve…

# Opportunity — Gerd Stolpmann, Jun 23, 2015

Gerd Stolpmann is looking for new Ocaml projects

Finally my job at Mylife ended. After all, it was a great success, and it used Ocaml as implementation language. The question is now: What is the next challenge?

Of course, this is a message to possible employers. There is now the opportunity to hire me, an Ocaml enthusiast of the first hour, creator of GODI, camlcity.org, and a number of Ocaml libraries. Also, I think I'm a quite good system programmer ;-)

Find mor…

# PlasmaFS — Gerd Stolpmann, Jun 23, 2015

A serious distributed filesystem

A few days ago, I released Plasma-0.4.1. This article gives an overview over the filesystem subsystem of it, which is actually the more important part. PlasmaFS differs in many points from popular distributed filesystems like HDFS. This starts from the beginning with the requirements analysis.

A distributed filesystem (DFS) allows it to store giant amounts of data. A high number of data nodes (computers with hard disks) can be attached to a…

# After NoSQL there will be NoServer — Gerd Stolpmann, Jun 23, 2015

An experiment, and a vision

The recent success of NoSQL technologies has not only to do with the fact that it is taken advantage of distribution and replication, but even more with the "middleware effect" that these features became relatively easy to use. Now it is no longer required to be an expert for these cluster techniques in order to profit from them. Let's think a bit ahead: how could a platform look like that makes distributed programming even easier, and t…

# Plasma Map/Reduce Slightly Faster Than Hadoop — Gerd Stolpmann, Jun 23, 2015

A performance test

Last week I spent some time running map/reduce jobs on Amazon EC2. In particular, I compared the performance of Plasma, my own map/reduce implementation, with Hadoop. I just wanted to know how much my implementation was behind the most popular map/reduce framework. However, the suprise was that Plasma turned out as slightly faster in this setup.
[Serbo-Croatian]
translation by Anja Skrba from Webhost…

# GODI is shutting down — Gerd Stolpmann, Jun 23, 2015

Sorry!

Unfortunately, it is no longer possible for me to run the GODI distribution. GODI will not upgrade to OCaml 4.01 once it is out, and it will shut down the public service in the course of September 2013.

This website, camlcity.org, will remain up, but with reduced content. Existing GODI installations can be continued to be used, but upgrades or bugfixes will not be available when GODI is off.

Although there are still a lot of GODI users, it is unavoidable to shut …

View older blog posts.