Select case studies
Libraries for Yatima Inc.
Yatima Inc. is a company that prioritises verifiable computation with a focus on zero-knowledge proofs. They have us implement a number of libraries for them:
Megaparsec. lean
A parser combinator library for Lean 4 programming language. The requirement was to have a library that is as close to Haskell's Megaparsec as possible. We have implemented it, skillfully negotiating the differences between Haskell and Lean typeclass system as well as strict evaluation model. The latter is implemented with Straume library.
Straume
A state of the art stream library for Lean 4 programming language. We have architected it from scratch with an aim to support larger-than-RAM data stream processing. It also supports infinite streams.
Webassembly runtime for Lurk Lab
Lurk Lab is a company that superceded Yatima Inc. It has implemented an innovative Lurk programming language. The first Turing-complete language, which produces zero-knowledge proofs.
We have implemented Wasm.lean, a webassembly runtime for Lean 4 language. The runtime is capable of running web assembly binaries compiled, for example, with Rust.
Then we have compiled it with yatima-lang, a compiler developed by Yatima Inc. Yatima-lang is a Lean 4 compiler that targets Lurk language. This allow to run web assembly binaries in Lurk runtime.
Ranking candidates for Yatima Inc.
Using a proprietary quantified methodology, we have helped Yatima Inc. hire Rust developers. Here is what the CEO of Yatima Inc. has to say about our work:
I can’t imagine how our team would be working without the positive vote from ZeroHR on those candidates that we ended up hiring. They are some of our best people.