Lambda the Ultimate

Harnessing Curiosity to Increase Correctness in End-User Programming. Aaron Wilson, Margaret Burnett, Laura Beckwith, Orion Granatir, Ledah Casburn, Curtis Cook, Mike Durham, and Gregg Rothermel. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems (CHI '03). (ACM paywalled link).

Despite their ability to help with program correctness, assertions have been notoriously unpopular--even with professional programmers. End-user programmers seem even less likely to appreciate the value of assertions; yet end-user programs suffer from serious correctness problems that assertions could help detect. This leads to the following question: can end users be enticed to enter assertions? To investigate this question, we have devised a curiosity-centered approach to eliciting assertions from end users, built on a surprise-explain-reward strategy. Our follow-up work with end-user participants shows that the approach is effective in encouraging end users to enter assertions that help them find errors.

Via a seminar on Human Factors in Programming Languages, by Eric Walkingshaw. To quote Eric's blurb:

This paper introduces the surprise-explain-reward strategy in the context of encouraging end-user programmers to test their programs. Attention investment provides a theory about how users decide where to spend their attention based on cost, risk, and reward. Surprise-explain-reward provides a strategy for altering this equation. Specifically, it attempts to lower the (perceived and actual) costs associated with learning a new feature, while making the reward more immediate and clear.

Unstructured casting (e.g. Java, C#, C++, etc.) can be harmful to security.

Structured casting consists of the following:

1: Casting self to an interface implemented by this Actor
2: Upcasting
  a) an Actor of an implementation type to the interface type of the implementation
  b) an Actor of an interface type to the interface type that was extended 
3: Conditional downcasting of an Actor of an interface type to an extension interface type.  (An implementation type cannot be downcast because there is nothing to which to downcast.) 

Claim: All other casting is unstructured and should be prohibited.
Note that this means that an implementation cannot be subtyped although an implementation can use other implementations for modularity.

Edit: The above was clarified as a result of a perceptive FriAM comment by Marc Stiegler

Actor DepositOnlyAccount[initialBalance:Euro] uses SimpleAccount[initialBalance]｡ 
 implements Account using
     deposit[anAmount] →
        ⍠Account⨀SimpleAccount.deposit[anAmount]¶
          // use deposit message handler from SimpleAccount (see below)
     getBalance[ ] → ⦻¶      // always throw exception
     withdraw[anAmount:Euro] → ⦻§▮   // always throw exception

As a result of the above definition, DepositOnlyAccount⊒Account and
DepositOnlyAccount has message handlers with the following signatures:

        getBalance[ ] ↦ ⦻,   //  always throws exception
        withdraw[ ] ↦ ⦻,     //  always throws exception
        deposit[Euro] ↦ Void▮

The above makes use of the following:

Interface Account with
       getBalance[ ]↦Euro, 
       deposit[Euro]↦Void,
       withdraw[Euro]↦Void▮ 

Actor SimpleAccount[startingBalance:Euro]
  myBalance ≔ startingBalance｡
      // myBalance is an assignable variable
         // initialized with startingBalance
  implements Account using
     getBalance[ ] →   myBalance¶
     deposit[anAmount] → 
       Void                    // return Void
          afterward  myBalance ≔ myBalance+anAmount¶   
               // the next  message is processed with
                        //  myBalance reflecting the deposit
     withdraw[anAmount:Euro]:Void →
       (amount > myBalance) � 
          True ⦂ Throw  Overdrawn[ ] ⍌
          False ⦂ Void           //  return Void
                    afterward myBalance ≔ myBalance–anAmount ⍰§▮
                 //  the next  message is processed with updated myBalance