[Cryptography] Languages, languages

[Perry E. Metzger]

On Thu, 12 Jun 2014 14:50:56 -0700 Bear <bear at sonic.net> wrote:
> On Wed, 2014-06-11 at 11:09 -0400, Perry E. Metzger wrote:
> 
> > There is another distinct advantage to doing work in a functional
> > language that hasn't been mentioned so far, but I'll throw it out
> > there anyway -- it is currently much easier to do proofs and
> > formal verification over functional languages, and this is only
> > partially an artifact of the present tooling situation. I expect
> > this will become better over time, but that there will always be
> > a gap.
> > 
> 
> Indeed, the only way to do formal verification of imperative 
> systems using existing frameworks requires one to develop a 
> formal semantics for those languages - which is specifically
> a way of rendering the content of any 'imperative' program in
> a functional way.

I'm not sure I would phrase it quite that way, given that

a) Even functional languages need formal semantics if one is to do
formal verification, and
b) The formal semantics that have been produced for languages like C
tend to have a lot of associated machinery to model state.

I would probably restate that as "formal semantics are a way of
assigning a meaning to programs in formal logic, and the formal
systems used by people doing such work these days tend to be typed
lambda calculi, which are also functional languages".

Naturally in such systems it is more natural to express the semantics
of functional languages, but also, the semantics of functional
languages are just plain simpler in most cases.

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