Galois Blog

I worked on a blockchain that used formal methods as part of the development workflow. The development process was essentially writing a paper that formalised an algorithm or a protocol, an implementation in Agda that would generate Haskell (or written straight in Haskell), property based tests against the paper, and then a whole business analysis/QA side where there'd be a requirements matrix against the paper with unit/integration/end-to-end tests on the features too. So you'd end up with formally checked code, property based tests, unit tests, integration tests, end to end tests, manual checks, and a few other tools too. This was a pretty slow process but on the two major product releases I worked on, I can only remember one bug slipping through and that was patched before people realised (and not a major issue either). So I think this style of development can work if you can 1) afford it, 2) afford the time to do it, and 3) formulate the requirements in such detail upfront.

Here's an example of a formal method paper that explains how a specific protocol works: https://hydra.iohk.io/build/13099985/download/1/blockchain-spec.pdf

This is a fun example of doing something similar with Coq to build a porn browser: http://www.michaelburge.us/2017/08/25/writing-a-formally-verified-porn-browser-in-coq.html

And there are a couple companies out there that do this style of development as a consultancy - it's probably the closest to 'engineering' that software development can get…

I would check out https://pedestrianobservations.com/ for information on other but analogous cost disease.

Basically, no, it's not just a meme. American managerial culture (or even Anglosphere at large, as alleged there) really does suck. And no amount of crafty mechanism design gets around the fact that least exploitable system seems to be one where the civil service isn't maimed and the work is done in-house.

Basically government should fund some free software for various general purposes (or just do a decent UBI), and then any "consulting" should basically be public sector and free software sector exchanging best practices.

The higher end academic consulting (ARPA) is legit[1] and should still exist, but it shouldn't be defense specific, and like drug bounties basically should exist to smooth over the "research...development...product" gap --- development is severely sort-changed current since outside of DARPA and ARPA-E so much research that doesn't contribute to someone's rent-seeking agenda just lies wasted.

[1]: I suppose should say I once was an intern at https://galois.com/

Software Engineer/Researcher @ Galois | Portland, OR, Arlington, VA, Dayton, OH. Remote is also a possibility.

Galois is looking for software engineers and researchers that enjoy working on challenging problems in computer science. We work with organizations like DARPA to explore blue sky ideas and turn them into usable technology that guarantees trustworthiness where failure is unacceptable.

We own the company together (through an ESOP), we make important decisions as a group, we have a one-level flat organizational structure, and people get to choose what they work on. We love to learn and share what we know, and that’s a big part of how we approach R&D, so we have no hard requirements for previous experience with similar work.

We think working here is awesome (See https://lifeatgalois.com)

To apply: https://galois.com/careers/software-engineer/

Name me a single company that uses Haskell 2010. It's completely irrelevant.

But I'll leave you to argue with Vitaly Bragilevsky (speaking at Galois):

"Haskell is a big language" -- https://galois.com/blog/2018/11/teaching-haskell-in-the-real-world/

Or Paul Hudak, Philip Wadler, and Simon Peyton Jones:

"Haskell is a big language" -- https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/history.pdf (p.28)

Maybe those guys know something.

It's cool Haskell goes through a small IR. That doesn't make TH, rewrite rules, CPP, the million extensions, STG, the runtime, the gigantic syntax, or the quarter million SLOC implementation simple.

You can't prove that something is secure, because to be applicable in mathematics/computer science there has to exist a precise definition.

If someone is just saying "This is a formally verified protocol" without what they actually checked for, they are salespeople not mathematicians.

"The authors of the KRA paper were able to understand what the proofs were about, and why they don’t cover the KRACK vulnerability. Even though the original proofs didn’t reveal security flaws, a principled approach would use these proofs in order to discover where to look."

https://galois.com/blog/2017/10/formal-methods-krack-vulnerability/

I certainly agree that both groups have bridged the gap.

Haskell is one of the best tools available when you absolutely have to get programs correct. Companies like Galois[1] for example are big Haskell users. I think it's very practical.

Haskell has also renewed interest in a branch of mathematics, category theory, that has helped understand problems in mathematical foundations and recently even physics.

Also, not to quibble, but I think it's been around since the late 80s. I can check my library but I believe the original report (I have a hard copy) was issued on April fools day.

[1] http://www.galois.com/