Implicit actions & program correctness

Implicit actions & program correctness

[deadhacker]

Hi all.  I am an old programmer who is new to Ada.  (I do not use Ada on the job.)

In the Ada books I'm reading, there's an emphasis on correctness & early bug detection that I haven't seen in many other books.  It's led me to contrast that with what I see on the job.

On the job, we often use frameworks such as Spring (for Java) to "autowire" components.  It means that a lot of work is done implicitly by that framework.  As one who audits systems, that implicit work makes is _really_ difficult to be sure that I understand how the program works, much less to verify correctness.

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 guess another way to look at what I'm wondering is: In books about software engineering with Ada, I see lots of talk about correctness especially by moving bug detection to the compile phase.  How often can that actually be done?

(Full disclosure: These are kind of a dumb questions because I think I know what Ada programmers might answer, so I feel a little guilty about asking, but I still hope to learn something & engage in some interesting talk.)

Re: Implicit actions & program correctness

[deadhacker]

On Friday, May 15, 2020 at 10:45:14 AM UTC-7, deadhacker wrote:
> Hi all.  I am an old programmer who is new to Ada.  (I do not use Ada on the job.)
> 
> In the Ada books I'm reading, there's an emphasis on correctness & early bug detection that I haven't seen in many other books.  It's led me to contrast that with what I see on the job.
> 
> On the job, we often use frameworks such as Spring (for Java) to "autowire" components.  It means that a lot of work is done implicitly by that framework.  As one who audits systems, that implicit work makes is _really_ difficult to be sure that I understand how the program works, much less to verify correctness.
> 
> 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 guess another way to look at what I'm wondering is: In books about software engineering with Ada, I see lots of talk about correctness especially by moving bug detection to the compile phase.  How often can that actually be done?
> 
> (Full disclosure: These are kind of a dumb questions because I think I know what Ada programmers might answer, so I feel a little guilty about asking, but I still hope to learn something & engage in some interesting talk.)

Addendum to my own post: As well as mentioning error detection at compile-time, I should have also mentioned making things explicit.  To me so far, a prominent essence of Ada appears to be "make things straightforward & explicit".  Very different from "autowiring" components.

Re: Implicit actions & program correctness

[Nasser M. Abbasi]

On 5/15/2020 12:45 PM, deadhacker wrote:
lar practices?  Have you been able to talk people into ending them?
> 
> I guess another way to look at what I'm wondering is: In books about software engineering with Ada, I see lots of talk about correctness especially by moving bug detection to the compile phase.  How often can that actually be done?


This is because in Ada, since it is strongly typed language, the
compiler can find more bugs at compile time, (for example,
when adding apples to oranges) which in other languages might not be
found at compile time, or it might needs the right
set of compiler switches (if they exist) added to find these bugs.

It means in Ada one spends more time getting the program to correctly
compile with no errors.

But it also means there is less chance of run-time errors.

In other languages, one spends much less time getting the program
to compile and more time trying to find the bugs that show up
when the program runs.

--Nasser

Re: Implicit actions & program correctness

[Paul Rubin]

deadhacker <gstover@gmail.com> writes:
> I guess another way to look at what I'm wondering is: In books about
> software engineering with Ada, I see lots of talk about correctness
> especially by moving bug detection to the compile phase.  How often
> can that actually be done?

Quite a lot, especially if you use fancier static checking like SPARK.
Programming errors can be classified into obvious silly ones, and more
subtle ones.  Decent compile time checking can catch most of the silly
ones.  That helps reliability and decreases testing workload, even if
you still have to deal with the remaining errors the usual ways.

Re: Implicit actions & program correctness

[Jeffrey R. Carter]

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

Re: Implicit actions & program correctness

[deadhacker]

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.  And since those other classes might also contain references to other classes, it makes those, too.  There are notations in the code or a config file (or both) that tell the framework what classes it's concerned with, but it creates the instances & makes sure they know about each other.

In my opinion, it's a cute trick for experiments, but it's inappropriate for production code, at least long-lived code that'll be the product of many programmers over the years.

More realistically, a web server might have a concept of a chain of filters that operate on a request.  Maybe we have an Authentication filter, an Authorization filter, a MakeSureItsNotSpam filter, & they have to be called in the right order.  When I'm auditing the program, it's difficult to be sure that all the filters are in the correct order or even all are included in the chain.

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?

Re: Implicit actions & program correctness

[Paul Rubin]

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/

Re: Implicit actions & program correctness

[Niklas Holsti]

On 2020-05-15 20:45, deadhacker wrote:

> Hi all.  I am an old programmer who is new to Ada.  (I do not use 
> Ada on the job.)
> 
> In the Ada books I'm reading, there's an emphasis on correctness &
> early bug detection that I haven't seen in many other books.  It's
> led me to contrast that with what I see on the job.
> 
> On the job, we often use frameworks such as Spring (for Java) to
> "autowire" components.  It means that a lot of work is done
> implicitly by that framework.  As one who audits systems, that
> implicit work makes is _really_ difficult to be sure that I
> understand how the program works, much less to verify correctness.

My son programs in Java professionally, using Spring and I believe 
several other frameworks. When it works it's great; when it fails, you 
are in deep trouble, because the reasons for the misbehaviour are hidden 
somewhere in the framework and its complex implicit or automatic and 
dynamic behaviour. Usually the error is in your own misunderstanding of 
what the framework does and how it should be used, but that doesn't help 
much.

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

There are ways to define some implicit behaviour in Ada. One can define 
default initial values for data of each type, and default values for 
subprogram parameters. One can define the procedure for default 
initialization of an object that has just been created, and the 
procedure for finalization of an object about to be destroyed. But none 
of these is as implicit or extensive as "autowiring", I believe.

The only case that has been forbidden by Ada coding rules I have seen is 
the use of default values for subprogram parameters. It was considered 
better to force the programmer to write out the actuals for all 
parameters in each call, so as to increase the likelihood that the 
programmer has thought out what the actual parameter values should be in 
each call. However, even this rule has not been enforced for the less 
critical code -- say, test code. (And the rule would work well only if 
programmers were also forbidden from using copy-and-paste, which is 
another topic :-) .)

-- 
Niklas Holsti

niklas holsti tidorum fi
       .      @       .

Re: Implicit actions & program correctness

[Brian Drummond]

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

Re: Implicit actions & program correctness

[deadhacker]

On Friday, May 15, 2020 at 3:10:02 PM UTC-7, Paul Rubin wrote:
> You might like this article (not Ada specific):
> 
> http://blog.tmorris.net/posts/understanding-practical-api-design-static-typing-and-functional-programming/

Paul, thank you so much for the link.  It's good reading.

To me, seems that his third requirement is the tough one.  (Quoting it here: "If I call move on a tic-tac-toe board, but the game has finished, I should get a compile-time type-error. In other words, calling move on inappropriate game states (i.e. move doesn’t make sense) is disallowed by the types.")

It seems that if I have a Move subprogram that operates on a Game, it & produces another Game, I don't see how it could sometimes return a FinishedGame that can be detected at compile-time.  (It could return a Game that could be checked for Finished at run-time.)

Sadly, his Java API is no longer available, so I can't see how he solved it.

Do you (or anyone else here) know how it could be solved with Ada?

Re: Implicit actions & program correctness

[Niklas Holsti]

On 2020-05-25 23:15, deadhacker wrote:
> On Friday, May 15, 2020 at 3:10:02 PM UTC-7, Paul Rubin wrote:
>> You might like this article (not Ada specific):
>> 
>> http://blog.tmorris.net/posts/understanding-practical-api-design-static-typing-and-functional-programming/
>
>> 
> Paul, thank you so much for the link.  It's good reading.
> 
> To me, seems that his third requirement is the tough one.  (Quoting
> it here: "If I call move on a tic-tac-toe board, but the game has
> finished, I should get a compile-time type-error. In other words,
> calling move on inappropriate game states (i.e. move doesn’t make
> sense) is disallowed by the types.")
> 
> It seems that if I have a Move subprogram that operates on a Game, it
> & produces another Game, I don't see how it could sometimes return a
> FinishedGame that can be detected at compile-time.  (It could return
> a Game that could be checked for Finished at run-time.)
> 
> Sadly, his Java API is no longer available, so I can't see how he
> solved it.
> 
> Do you (or anyone else here) know how it could be solved with Ada?

Checking such things was (and is) the goal of "typestate analysis", 
https://en.wikipedia.org/wiki/Typestate_analysis.

In Ada, it could be done statically with the precondition/postcondition 
system, plus some program proof. The Move operation would have a 
precondition "not Finished (Game)", and the prover would check that the 
program flow after any call of Move always ensures this precondition 
before Move is called again. Presumably this would be done by the 
program inspecting Finished (Game) in a control-flow condition, and 
allowing flow to a new Move call only in the "not finished" case.

Making this check "at compile-time" would of course require that the 
prover is always executed in or after any compilation.

-- 
Niklas Holsti
niklas holsti tidorum fi
       .      @       .

Re: Implicit actions & program correctness

[Paul Rubin]

deadhacker <gstover@gmail.com> writes:
> Sadly, his Java API is no longer available, so I can't see how he
> solved it.
> Do you (or anyone else here) know how it could be solved with Ada?

I didn't look at the Java code (don't know if it was posted somewhere)
but I'd expect it is done with Java classes and subclasses.  You'd have
a class for game state, and container (wrapper) classes for "initial",
"non-initial", "finished", and "non-finished".  Each wrapper would
either be empty, or contain a state of the specified type.

The "move" function would accept a non-finished state as a parameter,
and return three maybe-empty wrapper objects containing the new state.
To call "move" again you'd have to look in the "non-finished" wrapper to
get a non-finished state from it, in the event that there is one.  If
the non-finished wrapper is empty, then the game is finished and there
is no way to call "move" again.   Similarly with takeback, etc.

In Haskell, I did the exercise with numerically-indexed GADT's, but that
approach seemed hacky so I might try it again.

Re: Implicit actions & program correctness

[Niklas Holsti]

On 2020-05-26 1:31, Paul Rubin wrote:
> deadhacker <gstover@gmail.com> writes:
>> Sadly, his Java API is no longer available, so I can't see how he
>> solved it.
>> Do you (or anyone else here) know how it could be solved with Ada?
> 
> I didn't look at the Java code (don't know if it was posted somewhere)
> but I'd expect it is done with Java classes and subclasses.  You'd have
> a class for game state, and container (wrapper) classes for "initial",
> "non-initial", "finished", and "non-finished".  Each wrapper would
> either be empty, or contain a state of the specified type.
> 
> The "move" function would accept a non-finished state as a parameter,
> and return three maybe-empty wrapper objects containing the new state.
> To call "move" again you'd have to look in the "non-finished" wrapper to
> get a non-finished state from it, in the event that there is one.  If
> the non-finished wrapper is empty, then the game is finished and there
> is no way to call "move" again.   Similarly with takeback, etc.

That, of course, is basically a run-time check, and not a compile-time 
check as was originally desired. But as for Ada, program-proving tools 
could be applied at compile-time to verify that the program does check 
(at run-time) if "move" can be called again.

-- 
Niklas Holsti
niklas holsti tidorum fi
       .      @       .

Re: Implicit actions & program correctness

[Paul Rubin]

Niklas Holsti <niklas.holsti@tidorum.invalid> writes:
>> and return three maybe-empty wrapper objects containing the new state.
> That, of course, is basically a run-time check

I thought about it a little bit more and got rid of the wrappers, which
were ugly.  I'll post some Haskell code illustrating the idea if anyone
wants to see it.  But, even with the wrappers, it is a compile time
check in the sense that you have to extract the suitably typed board
state from the wrapper, before you can call the API function that
requires an arg of that type.  Thus, there is a compile time guarantee
that you can't call the API function with an illegal state.  That is
all that was asked for.