[Cryptography] Security proofs prove non-failproof

[Patrick Chkoreff]

Phillip Hallam-Baker wrote on 02/23/2017 06:41 PM:

> The biggest value I think there is to formal methods is actually in
> forcing people to design systems that are simple enough to be tractable.

Yes, a thousand times yes.


> I have removed about 10,000 lines of code from the Mesh code over the
> past year by refining the design.

I too count negative KLoCs as a positive measure of success.


> The tools I use do allow me to code at a very high level, which is very
> close to a specification language. My goal is to take the language in
> which I specify the problem as close as I can to the structure of the
> problem domain. 

That is why I write virtually all new code in the functional language I
implemented.  I find it very easy to write domain-specific abstractions,
all the way from generating balanced HTML tags:

  tag "div class=content" (...)

to even higher-level abstractions:

  standard_page "Title" (...)
  authenticate (\user_id ...)

I like to claim, tongue-in-cheek, that my entire accounting and
reporting system is written in 3000 lines of C with a 60K executable,
but I just have a really powerful config file language.


-- Patrick