Logic, Computer Graphics, OCaml, Rust, etc.
I've been working a fair amount on Moonpool . I think it occupies a fairly unique place in the new, vibrant OCaml 5 ecosystem and I'd like to explain why I think that. I'll compare it to generalist schedulers like Miou or Eio , to process-based parallelism libraries like Parany , and to domain parallelism libraries like Domainslib .
I've been working for years on sidekick , on my free time. It's getting tiresome to put so much effort into a project in the dark, so here's some basic journaling/rambles about it. So what's Sidekick? At first, and for a while, it was an attempt at writing a SMT solver, in OCaml, following the CDCL(T) paradigm, and in a functorized way. I've gone back on at least the…
( original title : "Curry Howard is a scam". See below.) The Curry-Howard correspondence has been talked about a lot recently, not only in Haskell circles, but also among CiC-based proof assistant practitioners (Coq, Lean, etc.). In a nutshell, it makes a deep parallel between "programs" (terms of some flavor of lambda calculus, typically), and "proofs" (these programs are a proof of their type,…
I've decided I want to resume blogging. So without further ado, here's a short piece about one of my side projects: benchpress (with a live hosting of the web ui ). In short, benchpress is a tool I use for running provers , by which I mean, generally, command-line tools that take a logic problem as input, and output something about the file such as "it's a valid theorem" or "it…
The glamorous world of SAT and SMT solvers is usually preoccupied with proving theorems, searching for software bugs, verifying hardware, and other similarly serious business. But today, we're going to solve Sudoku grids. My goal is to showcase mSAT , a parametrized SAT solver written in OCaml by my good friend Guillaume Bury and myself. The solver's code can be found on github , but…
Last October, I moved in Nancy to start working as an engineer with Jasmin Blanchette on an exciting project called Nunchaku . Since my domain is formal logic, I spend a lot of time manipulating, transforming, and traversing ASTs (abstract syntax trees). My primary method for debugging is pretty-printing structures; in nunchaku, I even have a --print-all flag to print the AST after each…
Greating, earthlings! Today I will present an exciting new OCaml library called maki . This post will be longer as usual, because it is actually two posts in one: first, I'll present the goals of Maki, sketch its design, and present the most salient parts of its API; then I will demonstrate how to use it to quickly build a (very naive) OCaml build system, featuring parallel build and cached…
A quick note about my current OCaml setup, in my last project, Nunchaku .
I have been hacking on the OCaml compiler recently; in particular, I added some support for coloring warning/error messages . At some point during the discussion over this pull request, it became clear that colored output should only be enabled if stderr was an interactive terminal (in opposition to a regular file handle or whatnot). The compiler does not link with the Unix library, so I…
For more than one year, vulnerabilies in software (especially pervasive C software) have been disclosed at an alarmingly high rate. I love OCaml, which is definitely safer, but still has gaps left open. I believe formal verification, albeit a very powerful tool, is not mature enough for most programmers (too difficult to use, requires too much efforts), so I'm thinking about alternative…
My PhD work is centered around automated theorem proving in first-order logic . This is obviously a very cool topic (otherwise I wouldn't have focused on it), so this post is a crash course (but the program won't crash because I use OCaml ) on one of the most classic method to prove (some) theorems automatically. I named... resolution ! The goal is to prove some (not too complicated)…
Some very common (and useful) operations, including the classic map , filter , and flat_map , traverse their whole argument and return another collection. When several such operations are composed, intermediate collections will be created and become useless immediately after. Languages like Haskell sometimes perform optimizations that merge together the operations so as to minimize the number of…
A quick survey of Lazy in OCaml I remember having heard that Jane Street had its own implementation of Lazy values, and that it was faster than the standard one. So I played a bit with several ways of managing lazy values in OCaml.
TL;DR : combinators and GADTs allow to describe types in abstract enough a way that they can be converted into/from various serialization formats. Edit : the code is now available in its own repository on github , and on my opam repository under the name CConv . Optional interfaces to Yojson, Sexplib and Bencode are also provided.
I've written, and am using, an OCaml module (see the documentation ) that is heavily inspired from Haskell's QuickCheck.
I've recently read an interesting article which shows an example of concurrency implemented in 3 differenet languages, namely Go, Erlang and C++. While the Erlang and Go examples seemed clear and concise, the C++ one looks long and hard to understand. The reason behind this complexity is that C++ does not provide a simple message passing primitive such as Go channels.
... is how you were born
Hi, I am shuba, and I'll be using this blog to dicuss various computer graphics topics I find interesting. I might also disgress on C++, which is my main programming language. For my first article, I'll try and answer a question that's not as simple as it seems: onto what did I click? How did the program know what I clicked on? We're used to be able to click on various kinds of…
The List.map function of the OCaml standard lib is not implemented tail-recursively. The current version (as of 4.00 on my computer) is let rec map f = function [] -> [] | a :: l -> let r = f a in r :: map f l
Rationale I'm starting a PhD on first-order automated theorem proving, which is the reason I'm writing an experimental theorem prover in OCaml. Theorem provers are full of complicated algorithms (that I plan to write on later), and my usual techniques for debugging are twofold: Writing a lot of assert to make sure invariants are not broken Printing debug information on stdout, if…
Hi there, here is the first post on this blag ! There will (or should, at least) be posts on technical subjects by several authors : shuba ; Vincent Doba; Simon Cruanes . We expect to write on C++ programming, functional programming, logic, graphics, etc. Cheers!