Homework 1 was worth a total of 18 points. Average: 15.7. 

* The Bookkeeping Problem was worth 1 point. 

* The Hoare response was worth 3 points. Students typically lost points for
poor English prose. I graded the written response as I would review an
article submission for a conference.  

* The Set Theory Problem was worth 2 points. 

* The Division problem was worth 2 points. You lost 1 point if you didn't
mention the division-by-zero problem. 

* The Large-Step Let problem was worth 2 points.

* The Small-Step Let Context/Redex problem was worth 2 points. 

* Having your Interpreter pass all of the example-imp-commands was worth 5
points. 

* Submitting a valid example-imp-command was worth 1 point. 

Example (Good-But-Not-Perfect) Written Response #1:

  In general, I found the principles behind Hoare's paper very appealing,
  while I found many of his specific suggestions be to strange and
  sometimes dated. On the surface, I agree with Hoare that the best way for
  a programming language to facilitate program design, documentation, and
  debugging is to be simple. If the language is not simple, then the user
  will have to spend too much of the design effort on deciding which
  features to use, possibly losing sight of what the program is actually
  supposed to do. Likewise, if the language is not simple, the difficulty
  of remembering how all of the different language structures work and
  interact makes it harder to read the code and debug any problems in it.

  However, Hoare and I seem to mean different things by "simple." This
  disagreement is shown most clearly in the way he praises many aspects of
  machine languages, such as fixed field formats and updating operations.
  Apparently, Hoare's simplicity means not having many complex features.
  Certainly, there is such a thing as too complex a feature . The Algol 60
  for statement from our other readings struck me as a fatally complex
  attempt to combine for, while, and for-each loops into a single
  structure, with the effect of making it much harder for a reader to tell
  what an Algol loop is doing. However, programming in languages with
  Hoare's kind of simplicity requires the programmer to keep many
  implementation issues (such as those enigmatically-praised fixed field
  widths) in mind while programming. I would argue that a properly
  "simple" language is one that frees the programmer from thinking
  about any issues other than solving the problem itself. Therefore, I
  would argue for the inclusion of many features that Hoare rules out as
  too expensive or complex but that serve to hide implementation details
  from the programmer.

Example (Good-But-Not-Perfect) Written Response #2:

  I don't believe that independent compilation is as big of a
  "band-aid" as Hoare makes it out to be. Programs written in modern
  object-oriented languages are split into fragments that naturally
  correspond to the various functional units / class code, so it is not as
  if programmers are being forced to arbitrarily fragment their code in
  ways that obfuscate the structure of the program. Additionally, he
  assumes that splitting code into separate binary modules will result in
  large and unwieldy interfaces in order to convey program state between
  modules.  Again, with modern object-oriented languages, data
  encapsulation obviates such interfaces.  Another of Hoare's arguments
  against independent compilation is the additional storage requirement for
  maintaining "bulky" intermediate code, yet one of his suggestions is
  to have the compiler dump its workspace and object code to disk in a
  "precompile" step. In my opinion (which was reinforced having just
  taken an optimizing-compilers course), the performance overhead of
  translation is mostly due to various optimization strategies.

  Hoare terms "security" as the criterion that a language design should
  not allow programming errors to give rise to machine or implementation
  dependent effects. I think language security is certainly broader than
  this; logically correct and error-free programs are often exploited by
  malicious third-parties because of nuances in the language
  implementation. We must consider that unintended behavior may not
  necessarily stem from incorrect program code, but rather from exploits in
  the language implementation.

  I completely agree with his opinion that general-purpose languages should
  provide the programmer with the ability to select or implement his own
  data structures / representations.  In my experience, simply changing the
  type of container for a collection of data (i.e., switching from a hash
  table to a linked list, or vice versa) makes a huge runtime difference
  for different data usage patterns (i.e., random-access versus iteration).
  Languages that infer types (especially containers and their
  implementations) make me apprehensive.

OCaml comments:

> if eb0 then eval_com c0 sigma else eval_com c1 sigma

Since OCaml has an expression-valued if, you can also write:  

>> eval_com (if eb0 then c0 else c1) sigma 

>  if (eval_bexp cond sigma)=true then

The "=true" isn't necessary: 

>>  if eval_bexp cond sigma then

>     if b1 then (eval_com c1 sigma ; eval_com c sigma) else sigma

This code only works because our state uses side-effects. You probably
want:

>>  if b1 then let sigma' = eval_com c1 sigma in eval_com c sigma' else sigma 

It is perfectly legal to use primes (') in ocaml variable names.