[scrape.yml] New OCaml Planet blog posts and videos (#3110)

Co-authored-by: cuihtlauac <[email protected]>

Author: github-actions[bot]

data/planet/anil/a-dsl-for-decentralised-identity-in-ocaml.md

@@ -0,0 +1,45 @@
+---
+title: A DSL for decentralised identity in OCaml
+description:
+url: https://anil.recoil.org/ideas/dsl-for-decentralised-id
+date: 2022-08-01T00:00:00-00:00
+preview_image:
+authors:
+- Anil Madhavapeddy
+source:
+---
+
+<h1>A DSL for decentralised identity in OCaml</h1>
+<p>This is an idea proposed in 2022 as a Cambridge Computer Science Part II project, and has been <span class="idea-completed">completed</span> by <a href="https://www.linkedin.com/in/michal-mgeladze-arciuch" class="contact">Michał Mgeładze-Arciuch</a>. It was co-supervised with <a href="https://patrick.sirref.org" class="contact">Patrick Ferris</a>.</p>
+<p>There are currently multiple identity providers without direct incentives to
+cooperate. This leads to many redundant implementations of the identity
+handling logic, many of which are not immediately compatible with each other,
+leading to additional increases in friction when eventual agreement needs to be
+reached to perform user actions.  Furthermore, from the perspective of the user
+of the identity service, they need to keep track of identity documents from
+multiple sources, which leads to more security attack surface.</p>
+<p>Solving the problem of partial identity proofs allows for many possible
+opportunities. For example, consider a simple May Ball ticketing system in
+which every college member gets a discount to their College, but without
+revealing their exact identity. Or imagine an e-commerce system, in which every
+user could prove their age to be over a given threshold, without revealing any
+additional information to the retailer.  In the example of a carbon credits
+project, we would be able to allow entities associated with any carbon
+offsetting project to prove their association, protecting the identity of
+whistleblowers.</p>
+<p>This project will build a system of Decentralised Digital Identifiers, which
+can be used to prove a subset of the information associated with the user’s
+identity using cryptographic proofs. Every participant in
+the system will have a public-private key pair associated with them. Then any
+identity provider P could provide an identity document for Alice, who has a
+public key A, by cryptographically signing a message containing both A, to
+point to the receiver of this document, and the document itself. Then, whenever
+Alice would want to authenticate herself to a service provider S, she could do
+so simply by sending the message she received from P to S. Then the service
+provider can verify that P, indeed supplied Alice with the given identity
+document.</p>
+<p>This Part II project was successfully completed but not available online; please
+contact the author for a copy of it. <a href="https://www.linkedin.com/in/michal-mgeladze-arciuch" class="contact">Michał Mgeładze-Arciuch</a> has subsequently founded <a href="https://www.czechtradeoffices.com/se/news/czech-startup-yoneda-labs-raises-over-$100-million-to-revolutionize-chemical-reactions-with-ai">Yoneda
+Labs to revolutionize chemical
+reactions</a>!</p>
+

data/planet/anil/a-hardware-description-language-using-ocaml-effects.md

@@ -0,0 +1,44 @@
+---
+title: A hardware description language using OCaml effects
+description:
+url: https://anil.recoil.org/ideas/tracing-hdl-with-effects
+date: 2025-03-01T00:00:00-00:00
+preview_image:
+authors:
+- Anil Madhavapeddy
+source:
+---
+
+<h1>A hardware description language using OCaml effects</h1>
+<p>This is an idea proposed in 2025 as a Cambridge Computer Science Part III or MPhil project, and is <span class="idea-available">available</span> for being worked on. It may be co-supervised with <a href="https://kcsrk.info" class="contact">KC Sivaramakrishnan</a> and <a href="https://github.com/andrewray" class="contact">Andy Ray</a>.</p>
+<p>Programming FPGAs using functional programming languages is a very good fit for
+the problem domain. OCaml has the <a href="https://anil.recoil.org/notes/fpgas-hardcaml">HardCaml ecosystem</a> to
+express hardware designs in OCaml, make generic designs using the power of the
+language, then simulate designs and convert them to Verilog or VHDL.</p>
+<p>HardCaml is very successfully used in production at places like <a href="https://janestreet.com">Jane
+Street</a>, but needs quite a lot of prerequisite knowledge
+about the full OCaml language. In particular, it makes very heavy use of the <a href="https://github.com/janestreet/hardcaml/blob/master/docs/hardcaml_interfaces.md">module
+system</a> in
+order to build up the circuit description as an OCaml data structure.</p>
+<p>Instead of building up a circuit as the output of the OCaml program, it would
+be very cool if we could <em>directly</em> implement the circuit as OCaml code by
+evaluating it.  This is an approach that works very successfully in the <a href="https://github.com/clash-lang/clash-compiler">Clash
+Haskell HDL</a>, as described in this
+<a href="https://essay.utwente.nl/59482/1/scriptie_C_Baaij.pdf">thesis</a>. Clash uses a
+number of advanced Haskell type-level features to encode fixed-length vectors
+(very convenient for hardware description) and has an interactive REPL that
+allows for exploration without requiring a separate test bench.</p>
+<p>The question for this project is whether the new <a href="https://anil.recoil.org/papers/2021-pldi-retroeff">effect handlers</a>
+in OCaml 5.0 might be suitable for using OCaml as a host language for a tracing-style
+hardware description language.  We would explore several elements using OCaml 5:</p>
+<ul>
+<li>using effects for control-flow memoisation (see <a href="https://github.com/ocaml-multicore/effects-examples/blob/master/multishot/memo.ml">the example</a>)</li>
+<li>restricting arbitrary recursion using effect handlers</li>
+<li>ergonomic ways of encoding fixed-length vectors</li>
+</ul>
+<p>This project will require a deep interest in programming language design and implementation,
+and an enthusiasm for learning more about digital hardware. There are quite a few good
+<a href="https://anil.recoil.org/ideas/computational-storage-for-vector-dbs">usecases</a> for using heterogenous hardware like FPGAs these days.
+There's a great <a href="https://signalsandthreads.com/programmable-hardware/">Signals and Threads episode</a> on
+programmable hardware with <a href="https://github.com/andrewray" class="contact">Andy Ray</a> that should give you more useful background knowledge as well.</p>
+

data/planet/anil/an-imperative-pure-and-effective-specification-language.md

@@ -0,0 +1,42 @@
+---
+title: An imperative, pure and effective specification language
+description:
+url: https://anil.recoil.org/ideas/effective-specification-languages
+date: 2024-08-01T00:00:00-00:00
+preview_image:
+authors:
+- Anil Madhavapeddy
+source:
+---
+
+<h1>An imperative, pure and effective specification language</h1>
+<p>This is an idea proposed in 2024 as a Cambridge Computer Science Part II project, and is currently <span class="idea-ongoing">being worked on</span> by <a href="mailto:[email protected]" class="contact">Max Smith</a>. It is co-supervised with <a href="https://patrick.sirref.org" class="contact">Patrick Ferris</a>.</p>
+<p>Formal specification languages are conventionally rather functional looking,
+and not hugely amenable to iterative development. In contrast, real world
+specifications for geospatial algorithms tend to developed with "holes" in the
+logic which is then filled in by a domain expert as they explore the datasets
+through small pieces of exploratory code and visualisations.</p>
+<p>This project seeks to investigate the design of a specification language that
+<em>looks and feels</em> like Python, but that supports typed holes and the robust
+semantic foundations of a typed functional language behind the hood. The
+langage would have a Python syntax, with the familiar imperative core, but
+translate it into <a href="https://hazel.org">Hazel</a> code behind the scenes.</p>
+<p>Another direction to investigate is also translating the same code into OCaml 5,
+and use the new effect system to handle IO and mutability in the source language
+code. This would allow for multiple interpretations of the program to execute
+depending on the context:</p>
+<ul>
+<li>an interative JavaScript-compiled (or wasm-compiled) tracing version that records variable updates</li>
+<li>a high performance version that batches and checkpoints variable updates and deploys parallel execution</li>
+</ul>
+<h2>Background Reading</h2>
+<ul>
+<li><a href="https://hazel.org/papers/propl24.pdf">Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine</a>, PROPL 2024.</li>
+<li><a href="https://patrick.sirref.org" class="contact">Patrick Ferris</a>'s first year PhD report (available on request to students interested in this idea).</li>
+<li><a href="https://anil.recoil.org/papers/2021-pldi-retroeff">Retrofitting effect handlers onto OCaml</a></li>
+</ul>
+<h2>Links</h2>
+<ul>
+<li><a href="https://hazel.org">Hazel</a></li>
+</ul>
+

data/planet/anil/analysis-of-the-raft-consensus-protocol.md

@@ -0,0 +1,41 @@
+---
+title: Analysis of the Raft Consensus Protocol
+description:
+url: https://anil.recoil.org/ideas/raft-consensus
+date: 2012-01-01T00:00:00-00:00
+preview_image:
+authors:
+- Anil Madhavapeddy
+source:
+---
+
+<h1>Analysis of the Raft Consensus Protocol</h1>
+<p>This is an idea proposed in 2012 as a Cambridge Computer Science Part II project, and has been <span class="idea-completed">completed</span> by <a href="https://anil.recoil.org/news.xml" class="contact">Heidi Howard</a>.</p>
+<p>The Paxos algorithm, despite being synonymous with distributed consensus for
+a decade, is famously difficult to reason about and implement due to its
+non-intuitive approach and underspecification. In response, this project
+aimed to implement and evaluate a framework for constructing fault-tolerant
+applications, utilising the recently proposed Raft algorithm for distributed
+consensus. Constructing a simulation framework for our implementation would
+enable us to evaluate the protocol on everything from understandability and
+efficiency to correctness and performance in diverse network environments.</p>
+<p>In retrospect, the complexity of the project far exceeded initial expectations:
+reproducing research from a paper that was still under submission and was
+modified regularly proved a big challenge alongside Raft's many subtleties.
+Nevertheless, the project achieved optoinal extensions by using our work to
+propose a range of optimisations to the Raft protocol. The project successfully
+conducted a thorough analysis of the protocol and released to the community a
+testbed for developing further optimisations and investigating optimal protocol
+parameters for real-world deployments.</p>
+<h2>Related Reading</h2>
+<ul>
+<li><a href="https://raft.github.io/raft.pdf">In Search of an Understandable Consensus Algorithm</a>, Diego Ongaro and John Ousterhout</li>
+<li><a href="https://anil.recoil.org/papers/rwo">Real World OCaml: Functional Programming for the Masses</a></li>
+</ul>
+<h2>Links</h2>
+<p>The dissertation is available as <a href="https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-857.html">UCAM-CL-TR-857</a> in the Cambridge Computer Laboratory technical report series.  <a href="https://anil.recoil.org/news.xml" class="contact">Heidi Howard</a> continued work on Raft subsequent to submitting this project and published it later in the year as <a href="https://anil.recoil.org/papers/2014-sigops-raft">Raft Refloated: Do We Have Consensus?</a>.</p>
+<p>You can watch <a href="https://anil.recoil.org/news.xml" class="contact">Heidi Howard</a> talk about her work in a Computerphile video from 2016:</p>
+<iframe width="560" height="315" src="https://www.youtube-nocookie.com/embed/jn3DBzr--Ok?si=D0rbJYdhqMX37pBw" title="YouTube video player" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" referrerpolicy="strict-origin-when-cross-origin" allowfullscreen=""></iframe>
+<p><a href="https://anil.recoil.org/news.xml" class="contact">Heidi Howard</a> also continued to work on Raft and distributed consensus later:</p>
+<iframe width="560" height="315" src="https://www.youtube-nocookie.com/embed/Pqc6X3sj6q8?si=HuYcxC1crauL422C" title="YouTube video player" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture; web-share" referrerpolicy="strict-origin-when-cross-origin" allowfullscreen=""></iframe>
+

data/planet/anil/announcing-ocaml-labs.md

@@ -0,0 +1,130 @@
+---
+title: Announcing OCaml Labs
+description: Introducing OCaml Labs, a new project at Cambridge Computer Lab to develop
+  and improve the OCaml programming language.
+url: https://anil.recoil.org/notes/announcing-ocaml-labs
+date: 2012-10-19T00:00:00-00:00
+preview_image:
+authors:
+- Anil Madhavapeddy
+source:
+---
+
+<p>I’m very excited to announce <a href="https://anil.recoil.org/projects/ocamllabs">OCaml Labs</a>, the latest project
+to hit the Cambridge Computer Lab. As anyone that hangs out near me
+probably realises, I very much enjoy functional programming. My weapon
+of choice tends to be <a href="http://www.ocaml-lang.org">OCaml</a>, as it
+condenses <a href="http://events.inf.ed.ac.uk/Milner2012/X_Leroy-html5-mp4.html">decades of
+research</a>
+into a pragmatic blend of functional, imperative and object-oriented
+programming styles. What’s perhaps less well known are the steady
+<a href="http://www.ocaml-lang.org/companies.html">inroads</a> that OCaml has been
+making into mission-critical areas of industry. At <a href="http://ocaml.janestreet.com">Jane
+Street</a>, billions of dollars of
+transactions are routed through a huge ML code-base that is designed to
+catch bugs <a href="http://vimeo.com/14313378">at compile-time</a>. At
+<a href="http://github.com/xen-org/xen-api">Citrix</a>, the Xen management
+toolstack that powers
+<a href="http://blogs.citrix.com/2012/10/09/one-in-a-million/">millions</a> of
+hosts in the cloud is <a href="https://anil.recoil.org/papers/2010-icfp-xen.pdf">largely written in
+OCaml</a>. Facebook does
+sophisticated <a href="https://github.com/facebook/pfff/wiki/Main">static
+analysis</a> using OCaml over
+their vast PHP codebase to close security holes.</p>
+<p>The OCaml community is small but dedicated, but there is always more to
+do to improve the language and ecosystem. So, thanks to a generous
+platform grant from <a href="http://ocaml.janestreet.com">Jane Street</a>, we are
+launching a program to help with the open-source development of OCaml
+from Cambridge.</p>
+<p>The <em><a href="http://www.cl.cam.ac.uk/projects/ocamllabs/">OCaml Labs</a></em> are
+based in the <a href="http://www.cl.cam.ac.uk">Cambridge Computer Lab</a> and led
+my myself, <a href="http://www.cl.cam.ac.uk/~am21/">Alan Mycroft</a> and <a href="http://www.cl.cam.ac.uk/~iml1/">Ian
+Leslie</a>. We’re closely affiliated with
+other
+<a href="http://www.cl.cam.ac.uk/projects/ocamllabs/collaboration.html">groups</a>,
+and will be:</p>
+<ul>
+<li>
+<p>developing the OCaml Platform, which will bundle the official OCaml
+compiler from INRIA with a tested set of community libraries that
+refreshed every six months.</p>
+</li>
+<li>
+<p>working with the core OCaml team at INRIA’s
+<a href="http://gallium.inria.fr/">Gallium</a> group on the compiler, and with
+commercial partners like <a href="http://ocamlpro.com">OCamlPro</a> on tool
+development. OCamlPro are making some very impressive progress
+already with the <a href="http://opam.ocamlpro.com">OPAM</a> packge manager and
+<a href="http://www.typerex.org">TypeRex</a> IDE helper.</p>
+</li>
+<li>
+<p>supporting the online presence with more teaching material and
+content. Yaron, Jason and I are working hard on a <a href="http://realworldocaml.org">new
+book</a> that will be published next year,
+and the OCaml Web team (led by <a href="http://ashishagarwal.org">Ashish</a>
+and
+<a href="https://plus.google.com/109604597514379193052/posts">Christophe</a>)
+have made great progress on a <a href="http://www.ocaml-lang.org">brand new
+website</a> that we will move to the
+<code>ocaml.org</code> domain soon.</p>
+</li>
+</ul>
+<h3>Research efforts</h3>
+<p>Of course, it is difficult to hack on a language in a void, and we also
+<em>use</em> OCaml heavily in our own research. The other half of OCaml Lab’s
+goals are more disruptive (and riskier!):</p>
+<ul>
+<li>The upcoming first beta release of <a href="http://openmirage.org">Mirage</a>,
+which is an operating system designed for cloud and embedded
+environments, and is written almost entirely from the ground up in
+OCaml. The outputs of Mirage include a <a href="http://www.openmirage.org/blog/breaking-up-is-easy-with-opam">large number of
+libraries</a>
+which are usable separately, such as pure implementations of TCP/IP,
+DNS, SSH, DHCP and HTTP. The Xen hackers, led by <a href="http://dave.recoil.org">David Scott</a>, are out in force to integrate Mirage
+into their <a href="http://www.xen.org/xensummit/xs12na_talks/T2.html">next-generation</a>
+platform. Meanwhile, Raphael Proust is busy eliminating the <a href="https://anil.recoil.org/papers/drafts/2012-places-limel-draft1.pdf">garbage
+collector</a>
+with his cut-down “LinearML” variant.</li>
+<li>Working with our collaborators at the <a href="http://horizon.ac.uk">Horizon
+Institute</a> on privacy-preserving technologies
+such as
+<a href="https://anil.recoil.org/papers/2012-sigcomm-signposts-demo.pdf">Signposts</a>
+which let you build and maintain your own personal clouds that
+operate <a href="https://anil.recoil.org/papers/2011-icdcn-droplets.pdf">autonomously</a>
+from the central cloud. You can read more about our <a href="http://www.cam.ac.uk/research/features/privacy-by-design/">privacy-by-design</a> philosophy too.</li>
+<li>Extending OCaml to run on secure hardware platforms that doesn’t
+compromise on performance, using the MIPS64-based <a href="http://www.cl.cam.ac.uk/research/security/ctsrd/cheri.html">capability
+processor</a>
+that is being developed at at the Lab.</li>
+<li>The <a href="http://www.trilogy-project.org">Trilogy</a> was a hugely
+successful EU-funded effort on future evolution of the Internet, and
+resulted in <a href="http://trilogy-project.org/publications/standards-contributions.html">numerous
+RFCs</a>
+on subjects such as multipath-TCP. We’re partipating in the
+follow-up (imaginatively dubbed “Trilogy2”), and look forward to
+working on more structured abstractions for programming large-scale
+networks.</li>
+</ul>
+<h3>Getting involved</h3>
+<p>So, how can you get involved? We are initially advertising three
+positions for full-time developers and researchers
+(<a href="http://www.jobs.cam.ac.uk/job/-21662/">junior</a> and
+<a href="http://www.jobs.cam.ac.uk/job/-21942/">senior</a>) to help us get started
+with the OCaml Platform and compiler development. These aren’t
+conventional pure research jobs, and a successful candidate should enjoy
+the open-source development cycle (you retain your own copyright for
+your own projects). The Computer Lab offers a pretty unique environment:
+a friendly, non-hierarchical group in a beautiful city, and some of the
+best faculty and students you could hope to hang out with.</p>
+<p>And finally, there is a longer lead time on <a href="http://www.cl.cam.ac.uk/admissions/phd/">applying for
+PhDs</a>, but this is a great time
+to get involved. When I started at the Lab in 2002, a little project
+called <a href="http://xen.org">Xen</a> was just kicking off, and many of us had a
+wild (and oft great) time riding that wave. Get in touch with myself,
+<a href="http://www.cl.cam.ac.uk/~am21/">Alan</a>,
+<a href="http://www.cl.cam.ac.uk/~iml1/">Ian</a> or
+<a href="http://www.cl.cam.ac.uk/~jac22/">Jon</a> soon if you are interested in
+applying! There’s some more information available on the <a href="http://www.cl.cam.ac.uk/projects/ocamllabs/collaboration.html">OCaml Labs
+pages</a>
+about options.</p>
+