Writing a formally-verified image browser in Coq and Haskell (2017) | Hacker News Reader

Writing a formally-verified image browser in Coq and Haskell (2017)

michaelburge.us

90 pointslelf12 comments

> 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!

> Coq could generate data types

Not only data types, the code too.

Pretty fast C code.

> 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.

http://adam.chlipala.net/papers/FiatCryptoSP19/

> I wish it supported more!

C++17 https://github.com/mit-pdos/mcqc

Scala https://github.com/JBakouny/Scallina

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.

well, it has Coq in the title

It would be a bit unfortunate if you had just exhausted political capital to convince your employer it was acceptable to use something called "Coq."

Discussed at the time: https://news.ycombinator.com/item?id=15103603

well the term is used more liberally now and you will see things like food porn, unix porn. though i think they are talking about sex porn.

a actual definition would be a unhealthy or voyeuristic interest in a particular subject.

Seeing HN title Oh, that looks interesting!

proceed to open article link, reads title =_= o_o Well, that escalated quickly!

Kudos for reversing the usual reaction to the title discrepancy impression.

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.

Reply on news.ycombinator.com