Re: Implicit actions & program correctness

[Brian Drummond <brian@shapes.demon.co.uk>]

On Fri, 15 May 2020 13:13:18 -0700, deadhacker wrote:

> On Friday, May 15, 2020 at 12:03:39 PM UTC-7, Jeffrey R. Carter wrote:
>> On 5/15/20 7:45 PM, deadhacker wrote:
>> > 
>> > It makes me wonder what experienced Ada programmers think of work
>> > done implicitly by a program.  Have you run into similar practices? 
>> > Have you been able to talk people into ending them?
>> 
>> I'm not clear what you mean by "implicit actions". In Ada, a lot can be
>> done automatically by the process called "elaboration". This is
>> generally considered a good thing. It's not uncommon for everything in
>> significant programs to be done by elaboration.
>> 
>> On the other hand, elaboration doesn't doe anything that isn't
>> explicitly in the code, so maybe it isn't what you're thinking about.
>> 
>> On the gripping hand, things like user-defined assignment and indexing
>> and pre- and post-condition testing might be considered implicit
>> actions.
>> 
>> --
>> Jeff Carter "Who wears beige to a bank robbery?"
>> Take the Money and Run 144
> 
> Hi Jeffrey & everyone.  Here is what I mean by implicit actions
> 
> (pseudocode)
> class Dinner contains references to Salad, Entre, & Desert.
> 
> class Entre contains references to a Meat, a Bread, & whatever else
> 
> you get the idea for classes Salad & Desert.
> 
> I declare those classes but do NOT write code that creates instances.  I
> compile & link it all together with my "autowiring" library such as
> Spring.  When the program fires up, the library sees that I declared all
> of those classes, so it starts creating instances.  For Dinner, it'll
> need a Salad, an Entre, & a Desert, so it goes to create instances of
> them & make sure that the Dinner contains their references.  

I think implicit actions can be very helpful both to increase 
productivity AND enhance correctness, if they are built on solid 
foundations - by raising the abstraction at which we program.

And Ada provides pretty solid foundations - and supports many implicit 
actions already.

A couple of illustrations ... first, without solid foundations.

>class Dinner contains references to Salad, Entre, & Desert.

So I find myself dining on Caesar's Salad, a nice steak, and ... uh, the 
Sahara.

You might think I'm taking the mickey here, and yes I am, but I've 
recently seen a well known spreadsheet import a sequence of hexadecimal 
numbers from a CSV file, and translate 1000 into 300,000,000 because it 
implicitly misinterpreted the sequence of characters "3E8".


Now a more solid foundation : the Ada type definition for a ranged 
integer creates a lot of implicit actions : compile time range checks, 
"defensive programming" raising runtime exceptions, and loops that can 
never run off the end of the associated array.

Now all this "defensive programming" can be done explicitly in other 
programming languages, with enough diligence from the programmer to 
provide all the checks necessary, but there is surely very little debate 
that the compiler will make a much more reliable job of it - with no 
further effort from the programmer.

It raises the level of abstraction at which the programmer deals with 
integers. The hidden details are precisely implicit actions.

> 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.

Which would translate in the integer example (conceptually, not 
literally) to explicit range checks on an index before accessing the 
array. If those can be done implicitly - but securely. reliably and 
safely - better to have them implicit as allowed by Ada.

So OK, Ada can do this for integers. That's pretty trivial (and yet goes 
so wrong so often elsewhere) but can we do the same for higher level 
objects like emails, as in:
> if is spam, error elsif is not authenticated, redirect to authentication
> elsif is not authorized, error else vend the resource.
...?

Possibly. The trick is to ensure the abstraction mechanism provides the 
tools to make implicit actions safely. Easy for integers, so it got built 
into the compiler. For emails and more complex things, you're looking at 
abstract data types.

In Ada the basic tool is the package, which allows you to export a data 
type and the allowed operations on it - while keeping the type itself 
"private". 

What you can do with an email (like "order_processing" it) is specified 
in the package spec.

How that happens is hidden - implicit - outside the package spec, but 
explicit in one place only - inside the package body.

procedure order_processing(e: email) is 
begin
  if is spam, error elsif is not authenticated, redirect to authentication
  elsif is not authorized, error else vend the resource.
end;

For an example of a recognised industry guru (Joel Spolsky) monumentally 
missing the point, I thoroughly recommend reading this: 

https://www.joelonsoftware.com/2005/05/11/making-wrong-code-look-wrong/

It is an excellent and widely (and justly) praised article and well worth 
reading. But it is written from a point of view that doesn't embrace 
languages with decent type systems.

The core example he uses is how to recognise which strings in a web 
application are safe, and which are unsafe (potentially containing XSS 
attacks); and his recommendation essentially leads to Hungarian 
notation : sName (safe) vs usName (unsafe) leaving you to read through a 
half million line application looking for 
Write("Hello" & usName); -- clearly a bug
Write("Hello" & Name);   -- probably a bug
Write("Hello" & sName);  -- good

thus missing the point, which is:

type SafeString is new String;

procedure Write (S : String) is
begin
  raise Program_Error with "XSS vulnerability here";
end Write;

procedure Write (S : SafeString) is
begin
  -- actually write the string
end Write;

function Sanitise (S : String) return SafeString is
-- do whatever you need to reject XSS here

recompile, fix all the "Program Error will be raised here" warnings, ... 
job done.


> 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?

For a quick hack, maybe. 

Raising the abstractions, e.g. to make Writes safe in the above example 
takes some real design effort if you are to be reasonably confident that 
the abstractions are watertight (and Joel has some interesting comments 
on that too). But worth it for tasks over a certain size.

-- Brian