From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail
From: Paul Rubin <no.email@nospam.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Implicit actions & program correctness
Date: Fri, 15 May 2020 15:09:59 -0700
Organization: A noiseless patient Spider
Message-ID: <871rnk97ew.fsf@nightsong.com>
References: <d4cc5c66-b82a-4ef7-8e69-2fa9b7bd99a6@googlegroups.com>
	<r9mp29$6nd$1@dont-email.me>
	<3c545096-d000-4d09-b3fe-ad8530632457@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="c215815cbffcabd76343cdde74de4b36";
	logging-data="15618"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX19fvuRJAWu0lZqXSyzBMzcN"
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux)
Cancel-Lock: sha1:1Y7vdCV+xifbckbVJnyVOwkGOpE=
	sha1:JgOE0X7T3+S9ZHCrNSTIsoNBots=
Xref: reader01.eternal-september.org comp.lang.ada:58700
Date: 2020-05-15T15:09:59-07:00
List-Id: <comp.lang.ada>

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/