7 Ways to Approach Soundness and Completeness

Soundness and completeness are important concepts that regularly tangle people up for some reason.  So, here's several different ways to think about them.  Choose the one that makes sense to you!

Grace for the CS1 Language Wars

We just changed the language for our intro CS course.  That change will probably obscure the underlying pedagogical change we also made for almost anyone outside UBC looking at the courses.

(Side Note: What's the pedagogical change?  From the perspective of someone who has not yet taught the course: A move toward a heavily structured approach to programming in which analysis of the features of a problem naturally leads to the process of solution.)

The language wars in intro CS courses, often called "CS1" courses, are powerful, engaging, frightening, and frequently pointless things.

So, why bother talking about them here?

Because once you start thinking about what you want in a language for your preferred CS1 pedagogy, you rapidly start throwing around words like syntax, semantics, closures, state, mutability, ...  And, understanding and slinging terms like that are part of what CPSC 311 is all about :^)

So, check out Andrew Black, Kim Bruce, and James Noble's thoughts on the syntax of an in-production CS1 language called Grace, particularly the section labeled "Block Semantics".

Grace uses eager evaluation but wants to allow programmers to introduce their own control constructs.  So.. they need to provide a simple syntax for a particular kind of expression.  Which one?

Sounds like an exam question!

Cheers,

Steve

"Little Language" for Elections

I got off topic discussing HCI-related issues in the Alaska senatorial race and valiantly connected (or tried to) that topic with our course by discussing Ka-Ping Yee's PVote, voting machine software as a concise interpreter for a ballot specification language.  I warmly recommend browsing through PVote (and the rest of Yee's work, voting-related or not).  It's a fascinating project that touches on elections, security, and languages.

Cheers,

Steve

Daily, 2010/11/10: Why Types?

Today was so exciting!  First, we finished up the (untyped, by the way) lambda calculus.  Everything's a single-argument function definition, function application, or an identifier

Then, we intro'd types.

SKIing and the Lambda Calculus

It's an amazing property of computation that we reduce all of our data (of which there is a staggering variety) to sequences of bits.

It is even more amazing that we can reduce the language of computation to a similarly lean representation.

In class, we've reduced lists, numbers, booleans, control flow operators, continuations, and recursion down to three things: single-argument function definitions, single-argument function applications, and identifiers.

We didn't get a chance to discuss the fact that we can go further.

The S, K, and I "combinators" (simple little functions) are one such representation.  Here's their definitions:

I x = x
K x y = x
S x y z = (x z) (y z)