For 22 years now, graphical OSes have offered the same puny little single ref-cell as the model of the clipboard, i.e., the storage for the copy-paste mechanism. Yet most of the interaction I have with my computer is stack-shaped; start performing a task, realize it requires a sub-task, perform the sub-task, and return to the previous task. If I happen to have copied something to the clipboard which I am pasting in various places and then need to perform a sub-task in the middle, this single register may become trashed in the process, with a "user-save register policy" as my only recourse.
I know Microsoft Office has some sort of fixed-width-but-bigger-than-1 array for its clipboard, but it's only within Office, not OS-wide.
I'm not saying the design of a stack-based clipboard would be obvious--for example, I don't know how the system should know when to pop an item off the stack--but a single ref cell isn't enough.
Sunday, January 22, 2006
Tuesday, January 17, 2006
Sunday, January 08, 2006
Three productivity boosters
A few of my current favorite productivity boosters:
I'm still on the lookout for good calendar software. Ideally online and compatible with Apple iCal.
- Subversion - With CVS, I wasted a lot of time fretting about file names and directory structures, because it was such a pain having to muck with the repository when I changed my mind. I ended up not being able to prototype nearly as rapidly because I spent time trying to plan the overall structure of my code. Sometimes I'd even give up and go off to work on something else. With Subversion I just blithely give things whatever name and directory structure suits me at the moment and keep working.
- Voo2do - This is the best task-list and project management software I've found online so far. It's got the right features and no more: I can give tasks a name, an associated project, and optionally a priority, a deadline, and notes; then I can create custom views over a particular set of projects. And that's about it. Now I'm keeping all of my to-do lists for everything in one place. Since I've been in grad school, I've found I do a lot of task-switching between my various jobs, so being able to keep all my tasks listed in one place should help me maintain my priorities not just in the context of one job but amongst all of them.
- Procmail - You've just gotta keep separate folders for emails from separate projects.
I'm still on the lookout for good calendar software. Ideally online and compatible with Apple iCal.
Thursday, December 22, 2005
Expressions and statements
This post explaining the I/O monad to a newbie on the Haskell mailing list motivates it in terms of expressions and statements:
We have a[n] "evaluation machine" and a[n] "execution machine". The formerInteresting. Imperative languages like C distinguish expressions and statements syntactically, but with various implicit conversions between them, e.g., expression-statements and procedures that execute statements but then return values. Haskell separates statements from expressions with the type system, and keeps them apart more strictly (no pun intended). But in a sense they're both making the same distinction.
evaluates expressions, the latter executes I/O actions. When the program is
started, the execution machine wants to execute the actions from the "main to
do list".
Tuesday, December 20, 2005
12 Weeks With Geeks
This looks interesting:
I'm not sure what I'll think of it, because on the one hand they're billing it as a more honest look into the software development process, which should be informative, but on the other hand, the preview hints at a number of the myths computer people like to believe about themselves.
I find myself increasingly upset at the way people in software are portrayed both by the media and by themselves--as idiot savants, socially inept geniuses, lone ranger superheroes, and revenge-of-the-nerds underdogs. It's dangerously delusional, it fosters extreme anti-social behavior, allows for all sorts of irresponsibility and incredibly bad software, continually dissuades women from entering the field, and perpetuates the belief that each hacker can solve any problem alone with complete disregard and disdain for a century of progress and collective knowledge.
How long can we continue duping the world into relying on us to design the heart of every automated mechanism known to man? How long will people continue believing in the myth of the 15-year-old hacker genius while simultaneously decrying the unreliability of software before the cognitive dissonance finally cracks?
At any rate, I don't know if that's where this movie is going. You can only tell so much from a preview. But it should be very interesting, especially about the product lifecycle and management perspectives.
http://www.projectaardvark.com/movie/It features some of your favorite outspoken software evangelists, Joel Spolsky and Paul Graham.
I'm not sure what I'll think of it, because on the one hand they're billing it as a more honest look into the software development process, which should be informative, but on the other hand, the preview hints at a number of the myths computer people like to believe about themselves.
I find myself increasingly upset at the way people in software are portrayed both by the media and by themselves--as idiot savants, socially inept geniuses, lone ranger superheroes, and revenge-of-the-nerds underdogs. It's dangerously delusional, it fosters extreme anti-social behavior, allows for all sorts of irresponsibility and incredibly bad software, continually dissuades women from entering the field, and perpetuates the belief that each hacker can solve any problem alone with complete disregard and disdain for a century of progress and collective knowledge.
How long can we continue duping the world into relying on us to design the heart of every automated mechanism known to man? How long will people continue believing in the myth of the 15-year-old hacker genius while simultaneously decrying the unreliability of software before the cognitive dissonance finally cracks?
At any rate, I don't know if that's where this movie is going. You can only tell so much from a preview. But it should be very interesting, especially about the product lifecycle and management perspectives.
Try-catch-finally in Scheme
I need a little break from all this parsing crap. Let's have some macro fun. Here's a PLT Scheme version of Java's try-catch-finally. Note the use of symbolic literals, rather than the usual syntax-rules/syntax-case literals list. This is due to my philosophy on macro keywords.
Example use:(define-for-syntax (symbolic-identifier=? id1 id2)
(eq? (syntax-object->datum id1)
(syntax-object->datum id2)))
(define-syntax (try stx)
(syntax-case* stx (catch finally) symbolic-identifier=?
[(_ e (catch ([pred handler] ...)) (finally e0 e1 ...))
#'(dynamic-wind void
(lambda ()
(with-handlers ([pred handler] ...)
e))
(lambda () e0 e1 ...))]
[(_ e (catch ([pred handler] ...)))
#'(with-handlers ([pred handler] ...) e)]
[(_ e (finally e0 e1 ...))
#'(dynamic-wind void
(lambda () e)
(lambda () e0 e1 ...))]))
(try (begin (printf "hi")
(printf " there")
(printf ", world")
(newline)
(error 'blah))
(catch ([exn? (lambda (exn) 3)]))
(finally (printf "finally!~n")))
Monday, December 19, 2005
Dynamic scope
Now I'm confused by another aspect of JavaScript scope:
Update: Oh, I forgot to mention the with construct -- another instance of dynamic scope.
Update: Also note that this is not the same thing as the behavior of var. If we write this function instead:
Update: I think this settles it--it's pretty much what it looks like. In chapter 13 of ECMA-262, the dynamic semantics of a FunctionDeclaration is to create a new binding in the "variable object" (ECMA-262 terminology for an environment frame) upon evaluation of the declaration.
If you imagine an environment as a list of frames, then in a lexically scoped language, this is a statically computable list. In a language with dynamic scope, frames in the environment may be generated or mutated at runtime, so it's not statically computable. JavaScript has some of both, so there are some things you can know statically about a variable reference, and some things you can't.
Update: The saga continues... I realized that I couldn't actually derive the above example from the official ECMAScript grammar! I see that others have made this surprising discovery as well: you can't nest FunctionDeclarations beneath Statements. Furthermore, you can't begin an ExpressionStatement with a FunctionExpression. As a result, it's impossible to derive the above program.
However, in practice, JavaScript engines do appear to accept the program, and use the dynamic semantics from chapter 13 as I describe above. But for strict ECMAScript, I can't seem to produce an example. I thought I could still force the issue by placing the nested function at the top-level of the enclosing function body and conditionally returning. But I was thwarted by two more interesting phenomena. First of all, when a var declaration and a function declaration compete to bind the same identifier, the var always wins, apparently. So this always produces "default", regardless of the value of b:
Now I need to confirm these two more properties of the language with the spec.
var f = function() { alert("default") }
function test(b) {
if (b) {
function f() { alert("shadowed") }
}
f()
}Evaluate test(true), and you'll see "shadowed". Evaluate test(false), and you'll see "default". Apparently function declarations are another instance where JavaScript is not lexically scoped (in addition to this, arguments, and the behavior of references to unbound variables).Update: Oh, I forgot to mention the with construct -- another instance of dynamic scope.
Update: Also note that this is not the same thing as the behavior of var. If we write this function instead:
var f = function() { alert("default") };
function test(b) {
if (b) {
var f = function() { alert("overridden") };
}
f()
}Then with test(true) we still get "overridden", but with test(false) we get an error from trying to apply undefined as a function. In other words, in this example, we have normal lexical scope with hoisting.Update: I think this settles it--it's pretty much what it looks like. In chapter 13 of ECMA-262, the dynamic semantics of a FunctionDeclaration is to create a new binding in the "variable object" (ECMA-262 terminology for an environment frame) upon evaluation of the declaration.
If you imagine an environment as a list of frames, then in a lexically scoped language, this is a statically computable list. In a language with dynamic scope, frames in the environment may be generated or mutated at runtime, so it's not statically computable. JavaScript has some of both, so there are some things you can know statically about a variable reference, and some things you can't.
Update: The saga continues... I realized that I couldn't actually derive the above example from the official ECMAScript grammar! I see that others have made this surprising discovery as well: you can't nest FunctionDeclarations beneath Statements. Furthermore, you can't begin an ExpressionStatement with a FunctionExpression. As a result, it's impossible to derive the above program.
However, in practice, JavaScript engines do appear to accept the program, and use the dynamic semantics from chapter 13 as I describe above. But for strict ECMAScript, I can't seem to produce an example. I thought I could still force the issue by placing the nested function at the top-level of the enclosing function body and conditionally returning. But I was thwarted by two more interesting phenomena. First of all, when a var declaration and a function declaration compete to bind the same identifier, the var always wins, apparently. So this always produces "default", regardless of the value of b:
function test(b) {
var f = function() { alert("default") };
if (!b) {
f();
return;
}
function f() { alert("overridden") }
f()
}Second, nested function declarations appear to be hoisted to the top of the function body. So the following example always produces "overridden":var f = function() { alert("default") };
function test3(b) {
if (!b) {
f();
return;
}
function f() { alert("overridden") }
f()
}Curious. At any rate, the behavior of popular JavaScript engines (Firefox and Rhino) seem to be a generalization of ECMAScript (by allowing FunctionDeclarations to appear nested within Statements) that is consistent with the spec (by obeying the behavior specified by section 13).Now I need to confirm these two more properties of the language with the spec.
Gotcha gotcha
In "a huge gotcha with Javascript closures," Keith Lea describes an example function written in JavaScript with surprising behavior. But he misattributes the unexpected results to the language spec's discussion of "joining closures." The real culprit, rather, is JavaScript's rules for variable scope. Let me explain.
Here's Keith's example:
The answer is that, in JavaScript, all var declarations are hoisted to the top of the nearest enclosing function definition. So while x appears to be local to the for-loop, it is in fact allocated once at the top of the loadme function and in scope throughout the function body. In other words, the above function is equivalent to:
To get the desired behavior, you need to use nested functions instead of loops, e.g.:
Update: My suggested fix is really bad advice for ECMAScript Edition 3! I should never recommend using tail recursion in a language that is not properly tail recursive. If all goes according to plan for proper tail calls in Edition 4, my suggestion would be fine for that language. But today, you can't use tail recursion. Instead, you should use any of the existing lexical scope mechanisms in ECMAScript for binding another variable to the loop variable i.
Solution 1 - wrap the closure in another closure that gets immediately applied:
Here's Keith's example:
function loadme() {
var arr = ["a", "b", "c"];
var fs = [];
for (var i in arr) {
var x = arr[i];
var f = function() { alert(x) };
f();
fs.push(f);
}
for (var j in fs) {
fs[j]();
}
}We might expect the function to produce "a", "b", "c", "a", "b", "c", but surprisingly, it displays "a", "b", "c", "c", "c", "c"! Wha' happened?The answer is that, in JavaScript, all var declarations are hoisted to the top of the nearest enclosing function definition. So while x appears to be local to the for-loop, it is in fact allocated once at the top of the loadme function and in scope throughout the function body. In other words, the above function is equivalent to:
function loadme() {
var x;
var arr = ["a", "b", "c"];
var fs = [];
for (var i in arr) {
x = arr[i];
var f = function() { alert(x) };
f();
fs.push(f);
}
for (var j in fs) {
fs[j]();
}
}In this version, it's clear why the function behaves as it does: the closure is mutating a global variable every time it's called!To get the desired behavior, you need to use nested functions instead of loops, e.g.:
function loadme() {
var arr = ["a", "b", "c"]
var fs = [];
(function loop(i) {
if (i < arr.length) {
var x = arr[i];
var f = function() { alert(x) };
f();
fs.push(f);
loop(i + 1);
}
})(0);
for (var j in fs) {
fs[j]();
}
}Now x is truly local to the loop body, and the function produces "a", "b", "c", "a", "b", "c" as expected.Update: My suggested fix is really bad advice for ECMAScript Edition 3! I should never recommend using tail recursion in a language that is not properly tail recursive. If all goes according to plan for proper tail calls in Edition 4, my suggestion would be fine for that language. But today, you can't use tail recursion. Instead, you should use any of the existing lexical scope mechanisms in ECMAScript for binding another variable to the loop variable i.
Solution 1 - wrap the closure in another closure that gets immediately applied:
function loadme() {
var arr = ["a", "b", "c"];
var fs = [];
for (var i in arr) {
var x = arr[i];
var f = (function() {
var y = x;
return function() { alert(y) }
})();
f();
fs.push(f);
}
for (var j in fs) {
fs[j]();
}
}Solution 2 - wrap the loop body in a closure that gets immediately applied (suggested in the comments by Lars):function loadme() {
var arr = ["a", "b", "c"];
var fs = [];
for (var i in arr) {
(function(i) {
var x = arr[i];
var f = function() { alert(x) };
f();
fs.push(f);
})(i);
}
for (var j in fs) {
fs[j]();
}
}Solution 3 - wrap the closure in a let-binding (in JavaScript 1.7, currently implemented only in Firefox 2):function loadme() {
var arr = ["a", "b", "c"];
var fs = [];
for (var i in arr) {
var x = arr[i];
var f = let (y = x) function() { alert(y) };
f();
fs.push(f);
}
for (var j in fs) {
fs[j]();
}
}Solution 4 - ditch var entirely and only use let (again, currently specific to Firefox 2):function loadme() {
let arr = ["a", "b", "c"];
let fs = [];
for (let i in arr) {
let x = arr[i];
let f = function() { alert(x) };
f();
fs.push(f);
}
for (let j in fs) {
fs[j]();
}
}The moral of the story is that in ECMAScript Edition 4, let is a "better var", behaving more like you'd expect. But until you can rely on let as a cross-browser feature, you'll have to use solutions like 1 and 2.
Tuesday, December 13, 2005
Semanticist's cookbook
Is this a dumb idea? I'd like to create a semantic modeling wiki where people can describe various techniques for modeling different kinds of programs, programming languages, and programming language features mathematically. Sort of a clearinghouse or cookbook for semantics. It could feature links to literature, and various categorizations so that people could find recipes by following different paths. For example, a reader might discover the exception monad by alternatively searching for control features, or error handling, or denotational modeling, or monads, etc.
Perhaps a better-designed database would be more organized, but I think wikis are good for continuously reorganizing, as well as for community contribution.
The Semanticist's Cookbook. I like it!
Update: Stubbed at http://semanticscookbook.org.
Update: Maybe I'll install a wiki another time but I don't have time for this now.
Perhaps a better-designed database would be more organized, but I think wikis are good for continuously reorganizing, as well as for community contribution.
The Semanticist's Cookbook. I like it!
Update: Stubbed at http://semanticscookbook.org.
Update: Maybe I'll install a wiki another time but I don't have time for this now.
Tuesday, November 29, 2005
What makes a good paper?
Or: Theorems are the test cases of semantics
Good PL papers define their systems with enough greek symbols, funky operators, inference rules and the like (what Mitch calls "dirty pictures") to demonstrate depth and precision of intellectual content. Without proving subsequent theorems based on these systems, though, there's no evidence that these systems are actually consistent or even useful.
A programming language semantics is, as Mitch puts it, "a mathematical model for predicting the behavior of physical systems." One of its primary purposes is reasoning (at a particular level of abstraction) about programs written in that language. It's generally hard to prove that a semantics is "the right one" for the problem space, which is a fuzzy notion, but theorems raise its probability of being useful.
A semantics alone may at least convey information about a language, since math is often more concise and precise than English. But without being put into use, it's doubtful whether it is really a specification; it's far too easy to slip into specifics as an algorithm. Or at the other extreme, it may leave out too many details to address the salient issues in the problem space. And who knows what subtle errors are lurking within the language definition? The best way to ensure that a semantics accurately defines a language at an appropriate level of abstraction is to prove theorems with it.
Good PL papers define their systems with enough greek symbols, funky operators, inference rules and the like (what Mitch calls "dirty pictures") to demonstrate depth and precision of intellectual content. Without proving subsequent theorems based on these systems, though, there's no evidence that these systems are actually consistent or even useful.
A programming language semantics is, as Mitch puts it, "a mathematical model for predicting the behavior of physical systems." One of its primary purposes is reasoning (at a particular level of abstraction) about programs written in that language. It's generally hard to prove that a semantics is "the right one" for the problem space, which is a fuzzy notion, but theorems raise its probability of being useful.
A semantics alone may at least convey information about a language, since math is often more concise and precise than English. But without being put into use, it's doubtful whether it is really a specification; it's far too easy to slip into specifics as an algorithm. Or at the other extreme, it may leave out too many details to address the salient issues in the problem space. And who knows what subtle errors are lurking within the language definition? The best way to ensure that a semantics accurately defines a language at an appropriate level of abstraction is to prove theorems with it.
Friday, November 18, 2005
Monday, November 14, 2005
Values in Non-Strict Languages
In the literature on non-strict languages, the term "value" seems to be used in a different way. In call-by-value languages, we classify a set of normal forms that we define as the "values" of the language, and arguments to functions must evaluate to values before the functions can be applied. But because in call-by-name or call-by-need languages, you can pass arbitrary, unevaluated expressions to functions, the notion of a value is in a sense less critical. You still need to define the normal forms in order to determine when to stop evaluating the whole program (or when to stop evaluating arguments to primitives with strict positions). But interestingly, in The Implementation of Functional Programming Languages, Peyton Jones still refers to the expression that a function argument is bound to as the variable's "value" -- despite the fact that it may not be in weak head normal form. Apparently the term "value" is informally used to mean a variable's binding, whereas the final result of an evaluation is only referred to as a normal form.
Tuesday, November 01, 2005
A packrat parser for Scheme
Through some random poking around the web, I just discovered this packrat parser in R5RS Scheme. I need to check that out.
Update: That's a parser in Scheme, not a parser for Scheme. (Thanks, Mitch.)
Update2: Not entirely random, Noel, thanks. Though discovering Tony's files by URL munging certainly was random.
Update: That's a parser in Scheme, not a parser for Scheme. (Thanks, Mitch.)
Update2: Not entirely random, Noel, thanks. Though discovering Tony's files by URL munging certainly was random.
Saturday, October 22, 2005
Language that represent themselves
In studying macros, I've discovered a fundamental complexity in one axis of language design: making aspects of a language easily representable within itself hampers the plasticity of the language. That is, as soon as you make it easy to observe the internals of the language, any changes you make to the language become by definition observable. As a result, any time you add, remove, or change a language feature, you add must consider that feature's representation within the language and how it affects the semantics.
This is well known to designers of languages with reflection, and causes all sorts of ulcers for compiler writers. But it's also a pain for designers of macros. For example, every time you add a new type of expression to the language, macros must be able to consume and produce that type of expression. Scheme makes this easier by generally having just one kind of expression--but in reality, that's a lie! Definitions are different from expressions, and cause lots of subtle complexities.
This is well known to designers of languages with reflection, and causes all sorts of ulcers for compiler writers. But it's also a pain for designers of macros. For example, every time you add a new type of expression to the language, macros must be able to consume and produce that type of expression. Scheme makes this easier by generally having just one kind of expression--but in reality, that's a lie! Definitions are different from expressions, and cause lots of subtle complexities.
Tuesday, October 18, 2005
Contracts fall right out
Jacob Matthews came to town this past weekend for several events, and on Monday gave a fabulous talk at Northeastern on multi-language systems. The experience made me proud to be a member of both the Northeastern PRL and the PLT research family. Jacob's work looks like it could be very useful, and I hope to apply it to several of my research projects. And the presentation was fantastic: he was entertaining and charismatic, and our group was a lively and interactive audience.
He's been talking for some time about how when programs interact between typed and untyped languages, "contracts fall right out." I was looking forward to finding out how, and he kept telling me that once I saw it it would be obvious. It had sounded rather magical to me, but sure enough, about halfway through his talk it became totally obvious! If a typed language is to use an expression from an untyped language in any useful way, it'll have to have a dynamic check to make sure the expression really was of the right type. But of course, you can't in general dynamically check the type of a procedure, so contracts are a natural solution!
He's been talking for some time about how when programs interact between typed and untyped languages, "contracts fall right out." I was looking forward to finding out how, and he kept telling me that once I saw it it would be obvious. It had sounded rather magical to me, but sure enough, about halfway through his talk it became totally obvious! If a typed language is to use an expression from an untyped language in any useful way, it'll have to have a dynamic check to make sure the expression really was of the right type. But of course, you can't in general dynamically check the type of a procedure, so contracts are a natural solution!
Saturday, October 01, 2005
Don't evaluate under lambda
In the past, I've been unsure what Alan Kay meant whenever he talked about "late binding" being the key insight into the development of Smalltalk, an insight which he attributes to his reading of the Lisp 1.5 manual. I think what he's talking about is the idea that if you have some part of your program that contains a piece of data, but now you want the construction of that data to vary based on some particular condition of the dynamic execution of the program, wrap it in a procedure. Now you can dynamically generate the data instead of fixing it once and for all.
This is of course possible regardless of whether you're in an OO or FP framework; in the context of OO, he's referring to the idea that instead of a record with fixed fields, you use methods that dynamically return the values of the fields. In functional languages you can do the analogous thing by placing functions in the slots of records, or in general you can just replace any datatype α with (→ α).
You can also take this in arguably the wrong direction and base the dynamic generation of this data on the mutable state of the program (whether that's the mutable fields of the object the method belongs to, or the mutable state of variables in the closure of a procedure). So you can see how late binding could be seen as a gateway drug to overuse of mutation.
But more and more I appreciate the power and simplicity of this notion that the natural path a program follows as it gets more complex is to take the pieces that are fixed and abstract them; to take the constants and make them variable; to take variables and fields and turn them into procedures and methods.
This is of course possible regardless of whether you're in an OO or FP framework; in the context of OO, he's referring to the idea that instead of a record with fixed fields, you use methods that dynamically return the values of the fields. In functional languages you can do the analogous thing by placing functions in the slots of records, or in general you can just replace any datatype α with (→ α).
You can also take this in arguably the wrong direction and base the dynamic generation of this data on the mutable state of the program (whether that's the mutable fields of the object the method belongs to, or the mutable state of variables in the closure of a procedure). So you can see how late binding could be seen as a gateway drug to overuse of mutation.
But more and more I appreciate the power and simplicity of this notion that the natural path a program follows as it gets more complex is to take the pieces that are fixed and abstract them; to take the constants and make them variable; to take variables and fields and turn them into procedures and methods.
Post-Redirect-Get with the PLT web server
Here's a nice idiom easily expressed with the PLT servlet library. Typically in an interactive web application you'd like to respond to form submissions (via "POST") with a page that the user can safely refresh, i.e., a page delivered via "GET". As a result, most people recommend you use what's known as the "Post-Redirect-Get pattern," where the immediate response to a POST is a redirect to an ordinary GET page.
Look how beautifully this is expressed in PLT Scheme:
Look how beautifully this is expressed in PLT Scheme:
The send/suspend procedure reifies the current continuation as a web continuation URL. The redirect-to procedure generates a response that redirects the user's browser to the given URL. By combining the two, we simply redirect the user's browser right back to exactly the point in the computation where we are, the only difference being that we've now returned from a "GET" interaction instead of a "POST". Usage looks like:(define (redirect/get)
(send/suspend
(lambda (k-url)
(redirect-to k-url))))
(Added to the Scheme Cookbook.)(define (start initial-request)
(let ([request (send/suspend
(lambda (k-url)
... form ...))])
(redirect/get)
(let ([user (extract-binding/single
'user
(request-bindings request))])
`(html (head (title "Hi"))
(body (p "Hi, " ,user "! Hit refresh!"))))))
One-step reduction semantics a historical mistake?
Wow, I just discovered this thread where Thorsten Altenkirch declares small-step operational semantics a "historical mistake." Sometimes I forget how specific the research culture I'm a part of is; given how often I use small-step semantics and abstract machines, I just assume that's what everyone does. But there are many people who consider big-step semantics to be more "natural." (Whatever that means.)
What confuses me about the popularity of big-step semantics in the typed functional language community is that Matthias's approach to proving type soundness via subject reduction in a small-step operational semantics is by now the de facto standard technique.
Anyway, I honestly have no idea how you'd reason about non-trivial language features like continuations with a big-step semantics.
What confuses me about the popularity of big-step semantics in the typed functional language community is that Matthias's approach to proving type soundness via subject reduction in a small-step operational semantics is by now the de facto standard technique.
Anyway, I honestly have no idea how you'd reason about non-trivial language features like continuations with a big-step semantics.
Monday, September 19, 2005
How do we automate?
Read this excellent and reasonable post from Jacob Matthews on undergraduate curriculum in computer science.
Let me call attention to Jacob's characterization of CS: "computer science is fundamentally the study of how to best systematically solve problems." I think it's interesting to compare this to Knuth's definition of computer science (pp. 5-6) as the answer to Forsythe's question "what can be automated?" (With some quick googling I found a slight generalization of this formulation to the broader question "how do we automate?")
It's useful to place Jacob's definition in the context of our research culture. You could describe us as belonging to the academic diaspora of Matthias Felleisen, whose profound textbook How to Design Programs and corresponding pedagogy permeate our approach to computer science. (The book's title is an homage to Polya's How to Solve It, a landmark work in the history of mathematical pedagogy, which sought to elevate math education beyond the realm of black art by providing students with a systematic process for solving problems rigorously.) The HtDP approach to teaching computer science is to give students a repeatable process for solving problems--this is systematic both in the sense that students are given a dependable process that they can reliably use to solve new problems, and in the sense that expressing the solution in terms that a computer can execute and evaluate is more formal and reliable than a rote hand-calculation.
Nevertheless, I like Knuth's and Raatikainen's definitions. Computer science is not always about problems--both in research and industry, I think there's a place for exploration where the discovery of applications may not follow until later. The real common thread seems to be the ability to describe any process in a formal way so that it can be specified without unnecessary implementation detail and yet in a way that it can be repeated reliably.
Let me call attention to Jacob's characterization of CS: "computer science is fundamentally the study of how to best systematically solve problems." I think it's interesting to compare this to Knuth's definition of computer science (pp. 5-6) as the answer to Forsythe's question "what can be automated?" (With some quick googling I found a slight generalization of this formulation to the broader question "how do we automate?")
It's useful to place Jacob's definition in the context of our research culture. You could describe us as belonging to the academic diaspora of Matthias Felleisen, whose profound textbook How to Design Programs and corresponding pedagogy permeate our approach to computer science. (The book's title is an homage to Polya's How to Solve It, a landmark work in the history of mathematical pedagogy, which sought to elevate math education beyond the realm of black art by providing students with a systematic process for solving problems rigorously.) The HtDP approach to teaching computer science is to give students a repeatable process for solving problems--this is systematic both in the sense that students are given a dependable process that they can reliably use to solve new problems, and in the sense that expressing the solution in terms that a computer can execute and evaluate is more formal and reliable than a rote hand-calculation.
Nevertheless, I like Knuth's and Raatikainen's definitions. Computer science is not always about problems--both in research and industry, I think there's a place for exploration where the discovery of applications may not follow until later. The real common thread seems to be the ability to describe any process in a formal way so that it can be specified without unnecessary implementation detail and yet in a way that it can be repeated reliably.
Subscribe to:
Posts (Atom)


