[Cryptography] Programming language technology (was Re: "NSA-linked Cisco exploit poses bigger threat than previously thought")

[Perry E. Metzger]

On Fri, 26 Aug 2016 21:05:10 -0700 Henry Baker <hbaker1 at pipeline.com>
wrote:
> Part of your job as a programmer is to help convince the compiler
> that certain checks -- that the compiler couldn't prove on its own
> were redundant -- can be removed after noticing various "assert"
> statements/expressions.  Now the "assert" statements themselves
> must also be proven to be redundant prior to eliding their run-time
> tests, but by sprinkling these "assert" statements liberally
> throughout the code, an assertion checked outside of a loop (which
> is checked but once) can often allow the compiler to deduce that
> the checks *inside the loop* are redundant and can then be removed
> without sacrificing safety.

We could do much better still now that dependently typed languages and
the like have been invented. Incredible strides have been made in
both the theory and practice of programming language and language
system design in recent years. Unfortunately most people are unaware
of this work.

Perry
-- 
Perry E. Metzger		perry at piermont.com