Re: Implicit actions & program correctness

[Paul Rubin <no.email@nospam.invalid>]

deadhacker <gstover@gmail.com> writes:
> I'd rather see explicit code like this:
> if is spam, error
> elsif is not authenticated, redirect to authentication
> elsif is not authorized, error
> else vend the resource.
>
> Seems that Ada, at least in the books I've been reading, nudges the
> programmer to work that way, so I was wondering what people with
> actual Ada experience have to say about it.  Does Ada nudge you to
> work that way?  And are you glad you do work that way?

Ideally you want to enforce those invariants at compile time, so you
don't have to do runtime checks.  You should only be able to vend given
an authorized request, where "authorized request" is a type, so the type
system enforces it.  Similarly to create an authorized request you have
to start with an authenticated one, etc.

You might like this article (not Ada specific):

http://blog.tmorris.net/posts/understanding-practical-api-design-static-typing-and-functional-programming/