• 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.

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

The Bitcoin Piñata - no candy for you — Hannes Mehnert (hannes), Apr 18, 2018

History

On February 10th 2015 David Kaloper-Meršinjak and Hannes Mehnert launched (read also Amir's description) our bug bounty program in the form of our Bitcoin Piñata MirageOS unikernel. Thanks again to IPredator for both hosting our services and lending us the 10 Bitcoins! We analysed a bit more in depth after running it for five months. Mindy recently wrote about whacking the Bitcoin Piñata.

On March 18th 2018, after more than three years, IPredator, the lender of the Bitcoins,…

Read more...

Whacking the Bitcoin Piñata — Mindy Preston, Apr 17, 2018

@yomimono or @hannesm surely know if people have tried crowbar on the BTC Piñata. – @kensan@mastodon.social

tl;dr - yes, and it seems that ocaml-x509 is not trivially easy to trick.

Background

The Bitcoin Piñata

In 2015 David Kaloper-Mersinjak and Hannes Mehnert released ocaml-tls, an implementation of TLS (formerly known as SSL) written fully in OCaml. A full writeup of the stack is available in their Usenix Security 2015 paper, and as a series of blog posts on mirage.io. To acc…

Read more...

Coq 8.8.0 is out — Coq, Apr 17, 2018

The final release of Coq 8.8.0 is available. It features better performances, tactic improvements, many enhancements for universe users, a new Export modifier for setting options, support for goal selectors in front of focusing brackets and a new experimental -mangle-names option for linting proof scripts. Feedback and bug reports are extremely welcome.

Taskforce on the Tezos Protocol, and Tzscan evolution — OCamlPro, Apr 13, 2018

As we are preparing to work on the Tezos Protocol, we’re still actively keeping the pace on the block explorer TZScan.io, adding cool information for baking accounts. We’d like to allow people to see who is contributing to the network and to understand the distribution of rolls, rights, etc.

For starters, we are showing the roll balance used for baking in the current cycle and the rolls history of a baker.

http://tzscan.io/tz1MqVR7hnZwH1FoQ7swjamanNxrXtNVAQ7v?default=baking

Enjoy, mo…

Read more...

OCaml Engineer for PL/distributed-systems cryptocurrency project at O(1) Labs (Full-time) — Functional Jobs (FunctionalJobs.com), Apr 06, 2018

O(1) Labs is a small, well-funded startup aiming to develop the first cryptocurrency protocol that can deliver on the promise of supporting real-world applications and widespread use. Our team is based in San Francisco, and we are funded by top investors (including Polychain, Metastable, and Naval Ravikant).

Cryptocurrency is a domain where correctness really counts. As such, a cornerstone of our approach is a focus on building reliable software through the use of statically-typed functional pr…

Read more...

How to quantify quantifiers: an Ltac puzzle — GaGallium (Armaël Guéneau), Apr 05, 2018

In some occasions, using the Coq proof assistant stops resembling a normal software development activity, and becomes more similar to puzzle solving.

Similarly to the excellent video games of the Zachtronics studio (TIS-100, SpaceChem, …), the system provides you with puzzles where obstacles have to be side-stepped using a fair amount of tricks and ingenuity, and finally solving the problem has often no other utility than the satisfaction of having completed it.

In this blog-post, I would li…

Read more...

OCaml JTRT — OCamlPro, Apr 01, 2018

This time of the year is, just like Christmas time, a time for laughs and magic… although the magic we are talking about, in the OCaml community, is not exactly nice, nor beautiful. Let’s say that we are somehow akin to many religions: we know magic does exist , but that it is satanic and shouldn’t be introduced to children.

Introducing Just The Right Time (JTRT)

Let me first introduce you to the concept of ‘Just The Right Time’ [1]. JTRT is somehow a ‘Just In…

Read more...

Full Time: Compiler Engineer at Jane Street in New York & London — GitHub Jobs, Mar 24, 2018

Jane Street is a proprietary quantitative trading firm, focusing primarily on trading equities and equity derivatives. We use innovative technology, a scientific approach, and a deep understanding of markets to stay successful in our highly competitive field. We operate around the clock and around the globe, employing over 500 people in offices in New York, London and Hong Kong.

The markets in which we trade change rapidly, but our intellectual approach changes faster still. Every day, we have …

Read more...

Full Time: Software Developer (Functional Programming) at Jane Street in New York, NY; London, UK; Hong Kong — GitHub Jobs, Mar 24, 2018

Software Developer

Jane Street is a proprietary quantitative trading firm, focusing primarily on trading equities and equity derivatives. We use innovative technology, a scientific approach, and a deep understanding of markets to stay successful in our highly competitive field. We operate around the clock and around the globe, employing over 500 people in offices in New York, London and Hong Kong.

The markets in which we trade change rapidly, but our intellectual approach changes faster still…

Read more...

Announcing the Sound Static Analysis for Security Workshop (2018-06-27 and 28 at NIST). See the whole programhere. — Frama-C, Mar 22, 2018

Coq 8.8+beta1 is out — Coq, Mar 19, 2018

The first beta release of Coq 8.8 is available for testing. It features better performances, tactic improvements, many enhancements for universe users, a new Export modifier for setting options, support for goal selectors in front of focusing brackets and a new experimental -mangle-names option for linting proof scripts. Feedback and bug reports are extremely welcome.

Release of Alt-Ergo 2.1.0 — OCamlPro, Mar 14, 2018

A new release of Alt-Ergo (version 2.1.0) is available on Alt-Ergo’s website: https://alt-ergo.ocamlpro.com/#releases. An OPAM package for it will be published soon.
In this release, we mainly improved the CDCL-based SAT solver to get performances similar to/better than the old Tableaux-like SAT. The CDCL solver is now the default Boolean reasoner. The full list of CHANGES is available here.
Despite our various tests, you may still encounter some issues with this new solver.  Please, don&…

Read more...

New updates on TzScan — OCamlPro, Mar 14, 2018

Update – TZScan.io can now work on top of the zeronet (zeronet.tzscan.io), we hope it can help the developers community monitor the network. You can now switch between the alphanet & zeronet networks!

OCamlPro is pleased to announce an update of TzScan (http://tzscan.io), its Tezos block explorer to ease the use of the Tezos network.

In addition to some minor bugfixes, the main novelties are:

  • Health of the network with stats about the blocks, endorsements, bakers, etc.
  • Display of futu…
Read more...

frama-clang 0.0.5, fixing compatibility issue with Debian/Ubuntu, is out. Download ithere. — Frama-C, Feb 19, 2018

Coq 8.7.2 is out — Coq, Feb 17, 2018

Version 8.7.2 of Coq is available. It fixes a critical bug in the VM handling of universes. This bug affected all releases since 8.5.

Other changes include improved support for building with OCaml 4.06.0 and external num package, many other bug fixes, documentation improvements, and user message improvements (for details, see the 8.7.2 milestone).

Release of a first version of TzScan.io, a Tezos block explorer — OCamlPro, Feb 14, 2018

OCamlPro is proud to release a first version of TzScan (http://tzscan.io), its Tezos
block explorer to ease the use of the Tezos network.

What TzScan can do for you :

– Several charts on blocks, operations, network, volumes, fees, and more,
– Marketcap and Futures/IOU prices from coinmarket.com,
– Blocks, operations, accounts and contracts detail pages,
– Public API to get information about blocks, operations, accounts and more,
– Documentation on different concept…

Read more...

OCamlPro’s Liquidity-lang demo at JFLA2018 – a smart-contract design language — OCamlPro, Feb 08, 2018

As a tradition, we took part in this year’s Journées Francophones des Langages Applicatifs (JFLA 2018) that was chaired by LRI’s Sylvie Boldo and hosted in Banyuls the last week of January. That was a nice opportunity to present a live demo of a multisignature smart-contract entirely written in the #Liquidity language designed at OCamlPro, and deployed live on the Tezos alphanet (the slides are now available, see at the end of the post).

Tezos is the only blockchain to use a strong…

Read more...

2017 at OCamlPro — OCamlPro, Jan 15, 2018

Since 2017 is just over, now is probably the best time to review what happened during this hectic year at OCamlPro… Here are our big 2017 achievements, in the world of blockchains (the Liquidity smart contract language, Tezos and the Tezos ICO,  etc.), of OCaml (with OPAM 2, flambda 2 etc.), and of formal methods (Alt-Ergo etc.)

In the World of Blockchains

The Liquidity Language for smart contracts

* Work of Alain Mebsout, Fabrice Le Fessant, Çagdas Bozman, Michaël Laporte

LiquidityOCamlPro dev…

Read more...

My 2018 contains robur and starts with re-engineering DNS — Hannes Mehnert (hannes), Jan 11, 2018

2018

At the end of 2017, I resigned from my PostDoc position at University of Cambridge (in the rems project). Early December 2017 I organised the 4th MirageOS hack retreat, with which I'm very satisfied. In March 2018 the 5th retreat will happen (please sign up!).

In 2018 I moved to Berlin and started to work for the (non-profit) Center for the cultivation of technology with our robur.io project "At robur, we build performant bespoke minimal operating systems for high-assurance se…

Read more...

MacOS package updated — Coq, Jan 09, 2018

The macOS installer for Coq 8.7.1 was updated on 2018-01-08 to fix frequent crashes of CoqIDE due to the use of an outdated dependency. Direct link to the new version: coq-8.7.1-1-installer-macos.dmg.

OCaml internships at LexiFi — LexiFi, Jan 08, 2018

LexiFi has great internship topics for OCaml hackers!

No prior knowledge of finance is required. If you are interested, please send your resume to careers@lexifi.com.

Posts and Talks Elsewhere — Mindy Preston, Dec 23, 2017

frama-clang 0.0.4, compatible with Frama-C 16 is out. Download ithere. — Frama-C, Dec 21, 2017

Coq 8.7.1 is out — Coq, Dec 15, 2017

Version 8.7.1 of Coq is available. It brings compatibility with OCaml 4.06.0, many bug fixes, documentation improvements, and user message improvements (for details see the 8.7.1 milestone).

testing ocaml-migrate-parsetree with `ppx_deriving_crowbar` — OCaml Labs, Dec 14, 2017

testing ocaml-migrate-parsetree with ppx_deriving_crowbar

Early feedback on Crowbar suggested that some automated method of constructing generators might be useful. It wasn’t necessary to do this immediately for the demonstration of testing the OCaml standard library’s Map and Set functors with Crowbar, but what about more complicated types? Like, say, the complicated and heavily mutually recursive types that compose OCaml parsetrees?

With an eye to solving this problem, I looked into a …

Read more...

Spartan type theory — Andrej Bauer, Dec 11, 2017

The slides from the talk “Spartan type theory”, given at the School and Workshop on Univalent Mathematics.

Download slides with speaker notes: Spartan Type Theory [PDF]

How to migrate your ppx to OCaml migrate parsetree — Shayne Fletcher, Dec 09, 2017

OCaml migrate parse tree

OCaml migrate parse tree

Earlier this year, this blog post [2] explored the implementation of a small preprocessor extension (ppx).

The code of the above article worked well enough at the time but as written, exhibits a problem : new releases of the OCaml compiler are generally accompanied by evolutions of the OCaml parse tree. The effect of this is, a ppx written against a specific version of the compiler will "break" in the presence o…

Read more...

Frama-C 16 - Sulfur is out. Download ithere. — Frama-C, Nov 28, 2017

Eighteenth OCaml compiler hacking evening at Pembroke, Cambridge — OCaml Labs compiler hacking, Nov 21, 2017

Our next OCaml Compiler Hacking event will be on Thursday 7th December in The Thomas Gray Room at Pembroke College, Cambridge.

If you're planning to come along, it'd be helpful if you could indicate interest via Doodle and sign up to the mailing list to receive updates.

When: Thursday 7 December 2017, 19:00 - 22:30

Where: The Thomas Gray Room, Pembroke College, Cambridge CB2 1RF

Who: anyone interested in improving OCaml. Knowledge of OCaml programming will obviously be helpful, but p…

Read more...

Migration to GitHub is complete — Coq, Nov 21, 2017

After several years of using GitHub specifically for its pull request system, the Coq development team has migrated the Coq bug tracker and Cocorico, the Coq wiki to GitHub as well.

More information about the migration of the Coq bug tracker may be found in this blog post.

More information about the migration of Cocorico, the Coq wiki, may be found on this wiki page.

Finally, the GitHub repository is now the repository we push to (as opposed to a mirror). Make sure that your git clone is tra…

Read more...

View older blog posts.