Avatar
Posts of varying effort on technology, cybersecurity, transhumanism, rationalism, self-improvement, DIY, and other stereotypical technologist stuff. Crazy about real-world functional programming.

OCaml as a security platform

OCaml is a strictly statically typed, type inferred, multi-paradigm-but-mostly-functional programming language. I’ll get into the nitty gritty of what that means later.

For now, if you’ve researched programming languages you’ve almost certainly heard of it, since it’s the goto platform for implementing compilers. But it’s also finding its niche in scientific computing, quantitative finance and some cryptocurrency projects. The reasoning here is that any edge in developing very complicated things, such as compilers, might give you an edge in other domains where complexity is high. Further still, others have learned that OCaml is not only good at making the hard things possible, but making the easy things easy (and safe!)

The purpose of this essay is to convince you that another niche OCaml is perfect for is security.

Security? Really?

Yes, security. Really. I’m not talking about firewalls or anti-virus software, or coming up with a security policy, or mandating best security practices. Those are important parts of the security story as well. But what I’m talking about here is as an implementation language for anything that’s important. If you have to write software that needs to be secure, you should be doing it in OCaml.

Some software is really important. Typically, it deals with sensitive information, or controls important processes, or has elevated privileges. That kind of software is usually pretty aggravating if it’s slow, and it’s disasterous if its logic is easily defeated. Those requirements are, unfortunately, often in conflict. Languages that are fast are often harder to implement logic in, and languages that are easier to reason about are often hard to run fast. Though with the modern language landscape the trade-off usually isn’t great: you can write something in, say, Go instead of C, and gain productivity wins without sacrificing too much speed, but the language is still difficult to reason about. Worse still, even very slow languages are still hard to reason about, they trade-off run-time performance for speedy development while still placing a superhumanly high burden on the programmer to get things right.

Temporal and spatial memory safety

Stuff here.

Immutable by default

Strong static types

Inferred types!

Algebraic data types

Invalid states should not be representable.

Safe concurrency

Monadic concurrency libraries like Async and Lwt allow closing off a whole world of concurrency bugs.

Capability extensions

That thing about effects.

All this and still fast!

all tags