4 ms·

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

90 points by lelf 7y ago

dang 7y ago
Discussed at the time: https://news.ycombinator.com/item?id=15103603 https://news.ycombinator.com/item?id=15103603
YayamiOmate 7y ago
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.
- Lowkeyloki 7y ago
  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.
Lowkeyloki 7y ago
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!
- lelf 7y ago
  > Coq could generate data types Not only data types, the code too.
- snaky 7y ago
  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/ http://adam.chlipala.net/papers/FiatCryptoSP19/
- lelf 7y ago
  > I wish it supported more! C++17 https://github.com/mit-pdos/mcqc https://github.com/mit-pdos/mcqc Scala https://github.com/JBakouny/Scallina https://github.com/JBakouny/Scallina
the_duke 7y ago
> 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.
nf05papsjfVbc 7y ago
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.
- skocznymroczny 7y ago
  well, it has Coq in the title
  - resoluteteeth 7y ago
    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."
reshie 7y ago
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.

90 points by lelf 7y ago

dang 7y ago

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

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.

Lowkeyloki 7y ago
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.

Lowkeyloki 7y ago

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!

lelf 7y ago
> Coq could generate data types Not only data types, the code too.
snaky 7y ago
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/ http://adam.chlipala.net/papers/FiatCryptoSP19/
lelf 7y ago
> I wish it supported more! C++17 https://github.com/mit-pdos/mcqc https://github.com/mit-pdos/mcqc Scala https://github.com/JBakouny/Scallina https://github.com/JBakouny/Scallina

the_duke 7y ago

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

nf05papsjfVbc 7y ago

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.

skocznymroczny 7y ago
well, it has Coq in the title
- resoluteteeth 7y ago
  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."

reshie 7y ago

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.