[Cryptography] I don't get it.

[Christian Huitema]

>> ". In a good programming language, it should be possible to statically assert 
> > your code is free of memory safety errors.
> 
> Really?  Statically?
>                X = array of foo[1..10];
>                Y = input(“What element do you want?”)[X::size]
> User types 11.

In the variant of C++ that we use at Microsoft, the "user types 11" scenario will absolutely be flagged by static analysis. The static analysis will learn that the array is size 10, and will complain if the program attempts to access it with an index that is not guaranteed to be in bounds. The programmer will be instructed to add bound checks.

I say "variant of C++" because we "decorate" the C++ code with SAL annotations, so that bound checking can be carried through procedure calls. At some level, you could say that the combination of C++ and SAL annotation defines a new language in which it is "possible to statically assert your code is free of memory safety errors."

-- Christian Huitema