Portland, OR (April 1, 2016) — Galois is known for building perfect software. But is our software too perfect?
The imperfect stitch, or Persian flaw, is a deliberate error in an otherwise perfect work of art. The term derives from the proverb, “a Persian rug is perfectly imperfect, and precisely imprecise.” It signifies the inherent humanity and imperfection of the artist. Nowadays, the term is used more generally; for example, Captain Jean Luc Picard’s Persian flaw is his inability to “sit down, shut up, and wait.”
With tools like Cryptol, SAW, and Copilot, Galois produces formally verified software day after day. So, we asked ourselves, does this perfection strip our engineers of their artistic creativity? Are our code and proofs void of the human touch?
Not any longer. Today, we are pleased to announce ISC, the Imperfect Stitch Compiler. ISC is the latest of Galois’s innovations.
Based on a collection of the developer’s personality traits along more than 20 dimensions, ISC introduces a subtle and unique bug in a software verification and implementation. The verification bug is made less obvious by innovative techniques such as slightly modifying the formal specification to differ from reality or adding antecedents until the precondition evaluates to false.
“ISC is very subtle,” commented one Galois engineer. “One bug took me over week to fix after accidentally enabling ISC during a test build.”
ISC has gone live, and interacts seamlessly with a variety of programming languages (including Haskell, ML, and Python) and verification engines (including SMT solvers, Coq, and Isabelle). At the time of writing, we have not developed a C interface, since nobody has ever written a bug-free C program in the first place.
Some quotes from our satisfied customers:
“I love guaranteed correct software, but it always felt so impersonal: it’s proven to always do one thing, and it’s the same for everyone! With my ISC-generated software, I know I have a unique, one-of-a-kind showpiece.”
“I’ve had a 20-year career in software testing. When our company started working with Galois, my job was on the line. Fortunately, with ISC, I can chase after that last, elusive bug. Thanks!”
“One word: authentic. When I started using Galois DSLs, my bug-free demos looked totally fake. With ISC we get those necessary hiccups that prove the authenticity of the work.”
“My ISC program works perfectly! Except for every once in a while… but then I just turn it off and back on again.”
Galois expects to release ISC from private beta on April 1, 2017.