Usually, I don’t get out much, but I did attend four big annual developer events in Seattle and presented in a few. All of these events have significant Microsoft presence and are sponsored by Microsoft directly or as part of its community outreach efforts.

ALT.NET Seattle

A informal social gathering of developers over a weekend in which developers vote on topics and break out into discussion groups, though some groups tend to have some leading the way and/or presenting.

Seattle Code Camp

A weekend in which developers from the community present code-focused presentations to the rest of the community.

Lang.NET Symposium

Lang.NET is a Microsoft-hosted symposium focused on programming languages and tools. It includes about half-Microsoft participation with the rest from industry.

DSL Dev Con

Chris Sell’s latest developer conference focused on DSL and following the Lang.NET symposium. His conferences usually takes a topic and aims to “fill the head” of the attendee. Chris picked out a dozen lectures, some by famous industry experts, over the course of one and half days, and included a guest panel discussion. This year the keynote was Martin Fowler, the father of DSLs. Another noteworthy presentation was by Intentional Software Corporation. Paul Vick provided the token Microsoft presence needed to justify the conference.

Some regular Seattle groups that I have attended in the past include:

NETDA user group meeting (one of the Seattle-area user groups focused on .NET).

Washington Technology Industry Association (focused on the technology business, but also contains a dev SIG).

MSDN Events (seasonal event in which Microsoft presenters rent out a theatre and present three lectures on Microsoft technologies du jour).

There was also the MVP summit for current MVP professionals.

Outside Seattle, the only conference I attend is the Software Industry Conference in Denver, Colorado, every summer.

Are there any others?

I came back from the Lang.NET conference and spoke to members of the C# team about two features which are exposed in IL, but are not available in C#.

1) Extended precision for floating-point calculations.

2) Tail call optimizations.

In C++, intermediate calculations can be performed at the highest precision offered by hardware. In C#, intermediate calculations with doubles are fixed at the standard or double precision--the precision of a double data type. The same is possibly true for floats. Double precision is not large enough to store a long value. The rationale is to prevents errors in which same code yields different results depending on optimization settings and environment.

Tail call optimizations arise when the result of a function call is directly returned without any intervening operations. The new function call reuses the caller’s stack frame and it’s use is not limited to tail recursion scenarios.

Tail calls are currently used by F# and Nemerle. C# programs benefit from tail call optimization in 64-bit architectures as tail calls are aggressively performed regardless of the presence of the .tail prefix. In 64-bit, the limited stack space is depleted much more quickly. Tail call optimization is turned off during debugging.

Because of the existing optimization in 64-bit, it seems harmless that the C# could automatically insert tail calls into the compiler in the VS 2010 timeframe. This would encourage programming in a more functional style. (Actually, tails calls are somewhat slower in x86.)

In my own development, I hit upon the stack limit through finite recursion and had to double the amount of stack space in my thread.

My current approach for dealing with these two problems is to disassemble my executable with ILDASM, insert the .TAIL prefix, remove the CONV.R8 or CONV.R4 instructions, and rebuild the executable with ILASM.

Some tail call links:

http://blogs.msdn.com/davbr/pages/tail-call-jit-conditions.aspx

https://beta.blogs.msdn.com/shrib/archive/2005/01/25/360370.aspx

Wolfram Research came out with a $250 Home edition of Mathematica. Regular licenses of Mathematic were expensive and out of reach for individual users, except in the academic market.

I used to own three different academic licenses of Mathematica in the past (1.0, 2.0, and 4.0) for the PC and Mac. I tried installing the last copy of Mathematica that I had and was unable to activate it, and the Mathematica support would not issue a new license because I was not a current student. I thought about paying for a course in the local community college just to get a student id, so that I can purchase an academic license of Mathematica, all for less than the price at retail.

This version is 7.0, and it follows quickly from version 6.0, which only seemed to have been released less than two years earlier. Apprehensively, some of the recent advances seem to touch on work that I have been doing, equational theorem proving in 6.0, sat-solving and discrete calculus in 7.0. Most recently, Wolfram Research have been working on a project called Wolfram|Alpha, a computational knowledge engine. I have always felt that it was a matter of time before the evaluation engine would be applied to natural language.

I have not had any instruction in formal methods, so I really didn’t encounter specification languages in my coursework, but I have read papers on proving programs including some classic papers by Hoare and Djikstra, and was familiar with Eiffel contracts.

At Harvard, I audited the first couple lectures of graduate level computer science course in Software Engineering, but never encountered modeling and specification in the initial lectures. (By the way, this instructor, a guest lecturer from industry, following custom, recounted his prior interactions with Bill Gates. He did indeed have Bill as a student, and proudly proclaimed in his opening lecture having given him a B years ago, waiting on us to form our own conclusions. Having earlier said that the Macintosh architecture was superior, his agenda was not in doubt. It didn't seem ethical for him to publish such confidential information, but then celebrities have less privacy rights.)

But, independently, I did arrive at a desire to express programming languages in a more mathematical way.

My first observation was that pseudo-code programs are actually real executable programs. The obstacles typically are the use of potentially large sets used as values and the use of a search or minimization function across said sets. The pseudocode for solving 2SAT above incorporates a nondeterministic choose operation and a several set operations.

While pseudo-code programs are lacking in implementation detail needed to execute in the most efficient way, such information could actually be automatically inferred by a compiler, or, if ambiguous time-space tradeoffs are involved, specifically included by the programmer as hints or performance guarantees to the compiler (in the form of contracts or attributes). There are actually very few core algorithms, which can be permuted in many ways.

Over the past couple years, I have become better acquainted with various specification languages, typically but not exclusively used in software verification. My interests in these languages rests in the similarities to the work I am doing with my own expression language (which I will henceforth refer to as "W"), which allows me to write programs in a more succinct mathematical style yet perform efficiently.

Many of these specification languages didn't actually exist during my college years, so I can't really fault my education. Joel, some time ago, talked at Yale about a software engineering course in Dynamic Logic, which turned him of from pursuing a graduate school in Computer Science.

Last year, as part of my continual self-improvements, I proceeded through the course material on software verification. I purchased and read through Software Abstractions- Logic, Language, and Analysis, which presented the Z specification language and also encountered the Z Notation: Reference Manual online. The reading left me with the impression that, at least in some methodologies, systems are designed first with a model program, written in some specification such as Z, which is checked either manually with proof-assistants or model-checking software and then consequently or concurrently ported into actual software. My self-study involved a course syllabus, purchase books in the reading lists, reviewing course notes/presentation and other material and last a few days. It made me more acquainted with a form of temporal logic in software verification--my prior exposure with temporal logic was within the context of natural language semantics--and also with the use of mu calculus in model checking, the technology that won its pioneering researchers the ACM Turing Prize last year.

Over the years, I have subscribed to and read papers from Microsoft Research, one of the few Microsoft feeds that I still read outside of MSDN blogs. Some papers refer to Horn-clause based language, pointing the use of a Prolog-equivalent systems. Microsoft dedicates significant resources to formal methods and verification. I have come across a couple of languages for specifications: AsmL (Abstract State Machine Language) and TLA+ (Temporal Logic for Actions).

Microsoft's AsmL also shares a lot of goals that I have except that it based on operational semantics rather denotational semantics.

AsmL is useful in any situation where you need a precise, non-ambiguous way to specify a computer system, either software or hardware. AsmL specifications are an ideal way for teams to communicate design decisions. Program managers, developers, and testers can all use an AsmL specification to achieve a single, unified understanding.

One of the greatest benefits of an AsmL specification is that you can execute it. That means it is useful before you commit yourself to coding the entire system. By exploring your design, you can answer the following questions: Does it do everything you intended it to? How do the features interact? Are there any unintended behaviors?

I was not initially fond of AsmL, but I do admire its resemblance to pseudocode. Below is an example specification for in-place sorting.

This program nondeterministically chooses two array items to swap until array is sorted. The choose operation closely resembles the pseudo code earlier. The loop continues until a fixed point is reached in which the next iteration of the loop produce further state changes; technically, though, the choose statement will actually fail before that occurs. By withholding detail, the algorithm can inclusively characterize both the quicksort and bubblesort algorithms according to the AsmL manual; however, these are unstable sorts which the specification disallows since distinct items that compare "equivalent" may be swapped.

I discovered TLA+ from a report that Microsoft's Oslo modeling language was reported to be based on TLA+ (Temporal Logic for Actions), although I haven't picked up on the similarities in any of the published Oslo information thus far. Joe Duffy recently also wrote about an internal research talk on TLA+ ("Math is nature's way of letting you know how sloppy your writing is") and points to a TLA+ website containing more information. TLA+ seems a bit unfriendly, and while it shares with my current work the integration of modal operators, its design shows that they are multiple ways to express the same idea. Don Box mention that one of the TLA+ architects is working in the Oslo group, but I sincerely hope that TLA+ is not Oslo’s future. It’s clear to me that Oslo will eventually evolve into richer programming model, potentially doing away with the code-behind XAML model.

My recent readings in the past few month included Software Engineering 1- Abstraction and Modelling   and Software Engineering 2- Specification of Systems and Languages which presents the RAISE specification language or RSL. I actually generally prefer this language, and seems most similar to the "W" I have been developing for so long--and initially conceived of since college.

One beneficial aspect of this exercise is seeing what operators I am missing. I noticed that RSL and W both include nondeterministic expressions. Which I have a single nondeterministic choice operator, RSL includes two with fine distinctions, and a related parallel operator. However, RSL does not have a Kleene star. I out-innovated RSL in generalizing the full regular expression operations (nondeterministic choice, Kleene star) over function composition rather than symbol concatenation. This allows me to represent and infer object invariants. I have only seen this used within the formal systems, Propositional Dynamic Logic and Interval Temporal Logic.

I have also become acquainted with other efforts such as CASL (Common Algebraic Specification Language) and VDM. VDM was the subject of a classic paper.  Developed by IBM in the 1970s and quite possibly the first specification language, there are now numerous tools including one that generates executables directly from the specification. Fred Brooks was probably influenced by this language, when writing his widely circulated paper, Mythical Man Month “No Silver Bullet,” which states that specifications, among other things, will never be a software engineering panacea.

The goal and the designs of the various specification languages diverge, but they help me to understand and refine the language W that I have built. My effort with W was inspired by the exposure to the alternative evaluation models yet common declarative presentation of the languages.

I found articulating how and why mathematics is important in computer science challenging. It’s always been my intuition--even more so, that they are interdependent -- but can I support this claim?

The importance of math is most clear in computer graphics because of the heavy use of linear algebra in rendering and even more so in ray tracing, yet this example is unsatisfying as it seems domain-specific and not an essential to the computer science.

I have wondered whether theoretical computer science is actually the natural progression of mathematics. Mathematics has been revolutionized through automated theorem provers, computer algebra systems and other packages that have mechanized previously human activities. Computers have even been successful in proving unsolved problems. It’s certainly clear that the practice of mathematics has improved considerable, but improvements in the process of performing mathematics is not satisfying argument for the important relationship of math and computer science, as computers have revolutionized numerous unrelated fields. I also considered whether theoretical computer science notions of algorithms, computable and recursive functions, and algorithmic behavior could unify computer science with mathematics.

Yet it all seems forced. A classmate, who took 1st place nationally in the Putman Mathematics competition, remarked that CS 51 to be the hardest course he took at Harvard; this surprised me as I didn’t find the programming assignments very challenging. His mathematical prowess provided little conceptual lift in the second of two introductory computer courses at Harvard. Grasping recursion and pointers is probably predicated on knowledge about stack frames and memory addressing, which I already had, having programmed significantly in assembly language.

If math and computer science are so related, then why does much of mathematics seem irrelevant to programming, for instance, calculus and differential equations? In the 1980s, computer science was still doubted as a serious theoretical discipline.

There is actually a subfield of mathematics, discrete mathematics, specifically focused on a grab bag of mathematical topics with relevant application to computer science. If much of mathematics seems not very relevant to computer programming, it is because the study of mathematics evolved to serve the fields of physics and engineering, which deals with continuous quantities, but current computer architectures can only deal with finite quantities and computer science is still a young field with consequently less influence over the development of modern mathematics. Perhaps future architectures may support continuous bits.

Fortunately, though, much of continuous mathematics have discrete analogues. Finite calculus serves the role for discrete functions as traditional calculus serves for continuous functions. Similar techniques from integration can be applied to symbolic summation, and similar techniques from differential equation can be applied to difference/recurrences equations. The natural base for discrete function is 2 instead of e, and the discrete logarithm function is the Harmonic function.

I can point to a few reasons why mathematics and computer science haven’t mixed so well. Programming languages and compilers are designed close to the hardware, and highly constrained to physical realities of the world.

My mathematical proclivities have lead me to embrace explicitly mathematical styles of programming such as functional (Lisp, Haskell), logical (Prolog III, λ Prolog, Mercury), and equational programming(Q/Pure, Mathematica), but I have always justified such approaches in their greater expressivity and potential performance advantages through high-level optimizations. Even imperative styles of programming can be handled through conversions into functions. Speaking of imperative languages, Fortress is a new language designed for mathematicians and scientists, that shows promise in making computer programs more like mathematics.

Languages can also be evaluated symbolically, which can potentially extract out answers without performing all the computations (much as a human being can walk through code and pick out the value of variable without evaluating every expression). In this mode of evaluation, programs can utilize operators that are possible in the larger computational sense but have no natural or efficient hardware implementation: continuous data types, modal operators, nondeterminism operators, nonterminating functions.  It always seemed to me that theoretical computer science was the study of computational operators.

It’s in this case of symbolically evaluating programs that the differences between mathematics and computer science begin to disappear in which programs and expressions are the same and their evaluation yields another reduced expression.

I have always believed in a vital relationship between mathematics and computer science. In fact, my second blog post in 2003 is also entitled “Math and Computer Science” and points to several arguments for a more incorporation of mathematics in computer science.

This belief was strengthened by being introduced to Lisp as my first formally taught computer science course, Artificial Intelligence, at Columbia University, taken during my senior year at high school. While I was already exposed to other high-level languages and assembly, the pedagogical impact of learning Lisp first is development of the strong associations between mathematics and programming such as a value-centric approach to programming. It was clear, for example, that the notion of first-class functions could provide a more generic way of programming, not to mention other ideas such as code as data, metacircularity, universal data structures. These associations were heavily strengthened by my purchase of Mathematica and my formal introduction to Prolog and ML, and their underlying mathematical foundation.

I actually became attracted to C++, because it seem like C was being enriched with a way to program in a more mathematical, high-level way with the introduction of operator overloading and OOP, but with an eye to performance. Some of this sentiment can be attributed to Stroustroup’s quasi-academic exposition of the language in the C++ Reference Manual.  I was still concerned that object-oriented mechanisms were deficient in its inability to express mathematical constructs such as set comprehensions or, more generally, a way to program using set theory, or alternatively to program in more logical style a la Prolog but without the limitations of Horn clauses and expensive searches. I wasn’t concerned as much with not be able to program in these alternate styles, as I was in the language’s inability to express mathematical notions.

At Harvard, reflecting my beliefs, I concentrated in applied math with emphasis in computer science (code words for majors and minors). I started out in computer science and applied math, but for procedural reasons and concerns that I was losing the math edge I had entering college, switched the two studies midstream—a decision I later regretted because the applied math requirements forced me to take courses outside computer science as a means of rounding out my mathematical toolset.

My knowledge in either computer science and mathematics is not as solid as I would like, as I have taken for effective half the number of courses in each discipline that a dedicated major would have taken. For instance, I audited courses in compilers and operating systems—normally two capstone CS courses--and read through the classic textbooks on the subjects, but I don’t have experience of completing projects, problem sets, and exams in those two areas.

On the other hand, some of my Applied Math courses could also fall under the Computer Science umbrella. Numerical Analysis deals with algorithms for problems of continuous mathematics. Abstract Algebra has a number of applications in in computer science such as cryptography and compression. For that course project, I wrote a full-fledged Mac application to solve the Rubik’s cube using group theory. It rendered the cube in 3d and showed all the rotations necessary to restore a cube; written using the Think Class Library framework and AppMaker designer, it was my first major application and I regret not release it as shareware.) My course in Operations Research dealt with topics like various optimization problems like linear programming, which make up Windows Solver Foundation.

Lately, I have been going through the course guides at Harvard and elsewhere to take an inventory of my knowledge set and proceed on a plan to study textbooks and online learning material from all of the missed courses in mathematics and computer science and related disciplines. Graduate courses are pedagogically efficient as the material tends to be more interesting while actively incorporating concepts introduced in undergraduate courses.

 Theory and Practice

My appreciation of mathematics in computer science was heighted by the rich theoretical treatment of computer science at Harvard. Great differences in textbooks I have surveyed (e.g., compare the “Dragon” book to other compiler books) indicate that is not true in most other schools, but as I can attest from auditing a Computational Linguistics course at UCLA, is probably true for the top schools. The Harvard CS department philosophy is to not teach technology, because such knowledge is transient, changing rapidly, in favor of more theoretical knowledge that will last a lifetime. In one course, the stated aim was to allow students to read academic papers in the field. While I agree with both of the aims, I think a general understanding of an area, beyond existing practice, is important in appreciating and advancing the field, and is not easily acquirable outside the university.

Programming languages and technology are not taught in Harvard courses, but something learned primarily on one’s own with help from “section,” hosted by teaching assistants. I find the mindset that one needs to go to school to learn technology quite amusing, but this may be the unfortunate outcome of teaching technology rather than theory.

The philosophy reflects a Harvard’s general predisposition to theory. Harvard does not have an majors in accounting, medicine, law or business, because of their practical nature. Future accountants and business students take economics, law students take government and medical students take biochemistry. Perhaps that is the right focus as an astonishing ninety percent of Harvard students eventually attain a graduate degrees. Stanford, Harvard’s polar opposite on the West Coast, was founded with a more pragmatic orientation with a more open to teaching technology. Stanford has a course on using multimedia applications and another on CS 193P: “IPhone Application Programming,” (perhaps the P refers to a professional course), neither of which would ever be admitted at Harvard, but then I noticed that Harvard's statistics department is guilty in offering Statistics 135: “Statistical Computing Software.”

Dare Osabanjo invoked a quote from Djikstra, “that computer science is no more about computers than astronomy is about telescopes” in response to Coding Horror post on the need for a more relevant computer science curriculum, which doesn’t seem to appreciate the differences between a computer science and software engineering. I am not sure that some of the suggestions such as deployment and source control, belong in either program at a top school.

I tried to dispel misconceptions of a reader, who aspired to attend a top university for very mundane programming reasons. I told him that my “Theory of Computation” course didn’t reference actual computers until the last week in which a “random access Turing machine” make theory more relevant. “Data Structures and Algorithm” included no programming, but rather was heavy on problem sets to prove properties about algorithms. My programming languages course didn’t discuss any popular programming language, but various mathematical formalisms. Harvard’s database course probably doesn’t teach SQL, but will probably give you the mathematical foundations, such as relational calculus and transaction processing, to build a database management system in the abstract.

After the heavy theory in school and being acquainted with papers on proving programs, I was somewhat disheartened by the absence and even distrust of mathematics or an academic theory in my actual work experience. Data structures were mostly limited to hash tables, arrays and linked lists, and programming felt much more like “glue” code.

I lament that I focused a lot more time on learning technology than theory during college, as I have found that technological knowledge depreciates quickly but yet never catches up to theory, yet I benefited from having used expensive $10K workstations and products so that when personal computers became unconstrained, I still came out ahead. As I have started working on advanced projects in natural language and static analysis, I found that computer science theory actually have serious applications, initially in designing my algorithms, and later, in directly representing and manipulating mathematical operators in memory.

I began writing a post on my ideas of the relationship between mathematics and computer science, which grew very long, so I am splitting the one long post in several, and I will just include links to each post here.

Table of Contents

1. Math and Computer Science
2. Unifying Math and Computer Science
3. Specification Languages

Before there were blogs and the web, I used to be an avid reader of magazines, subscribing to as many as thirteen in the early 1990s, many of them in computer programming, particularly the less popular, more technical magazines that I could not read in the libraries.

Eric Sink noted two years ago that computer magazines were dying, reflecting a larger trend in which nearly all paper media is declining amidst the technology boom.

Dr. Dobbs Journal, one of my early subscriptions, appears to be the latest developer magazine to disappear. I subscribed to about three different magazines on C/C++ programming including C++ Report and C/C++ User Journal, but it doesn't appear that any of them are still around. Byte went out of print fairly early, and Software Development magazine disappeared.

Microsoft System Journal still survives in the name of MSDN magazine from a merger with MIND magazine, but as Microsoft's official magazine for announcing new technologies, its future is guaranteed.