[odyssey7]

So, formal methods produce runnable systems, but communication remains the challenge.

If a formal spec is messy, then it's a proof of ... what, exactly?

A formal specification that bridges tech and product, that lets non-technical contributors read and discuss all the logical nuances, directly as operational code, at product's level of abstraction of interest, would transform a lot.

It's no longer a challenge to create code, it's a challenge to create business requirements and translate them into systems.

[rzmmm]

The spec and proof are separate. In this blog article he mentions seL4 formal verification, where they state that the spec was 4900 lines of Isabelle and the proof was 200K lines. Obviously human has to understand the spec deeply.

[jaggederest]

There's an information theoretic aspect about generating a proof which is essentially not human readable from 4900 lines of spec. I wonder how much additional signal they're getting out beyond what's in that 4900 lines, and what's the percentage of noise in the 200k lines of proof?