> It’s an unspoken truth that most large image databases people have are actually porn collections, so we’ll be honest with ourselves and call it a porn browser.
I wasn't aware Coq could generate data types for general purpose programming languages. According to the docs, it supports OCaml, Scheme, and Haskell. I think I may have spotted a plugin to generate C code as well. I wish it supported more!
> All formal reasoning is done in the Coq proof assistant, and the overall trusted computing base also includes a simple pretty-printer and the C language toolchain.
> We further demonstrate that simple partial evaluation is sufficient to transform into the fastest-known C code, breaking the decades-old pattern that the only fast implementations are those whose instruction-level steps were written out by hand.
> These techniques were used to build an elliptic-curve library that achieves competitive performance for 80 prime fields and multiple CPU architectures, showing that implementation and proof effort scales with the number and complexity of conceptually different algorithms, not their use cases. As one outcome, we present the first verified high-performance implementation of P-256, the most widely used elliptic curve. Implementations from our library were included in BoringSSL to replace existing specialized code, for inclusion in several large deployments for Chrome, Android, and CloudFlare.
If you've come to the comments before reading the article, please do observe the URL before clicking on it. The page (because of the title) might be flagged by keyword filters in workplace proxies.
The ol' bait and switch. But, I mean, it is technically an image browser. Despite the title, there's nothing in the design that limits the types of images this can be used for. In fact, I missed that distinction until your comment because I was mostly skimming.
