OK, now let's try that on Ubuntu 7.10:
$ ls/usr/lib | wc -l 1180 $ ls/usr/lib/*.so* | sed 's/\.so.*/\.so/' | sort -u | wc -l 462 Less than thousands if you rule out files that aren't shared libraries or that are just links to the same shared library; that includes the equivalents of the OS X frameworks. Note that/usr/lib contains a lot of subdirectories which you're missing; a better bet is the following:
$ ls -R/usr/lib/ | grep \.so | sort -u | wc -l 5748 Of course the exact numbers will vary depending on what you have installed, so YMMV and all that.
Some interesting comments in TFA regarding the "source" of Vista's performance issues:
In response to this, Microsoft made fundamental changes to the way Windows Vista was linked together; shifting more towards modular designs rather than the monolithic processes used in previous versions of Windows. This increased amount of componentization, while satisfying the DoJ and EU, also led to performance issues due to the increased number of libraries which comprise the operating system. On traditional hard drives, the more separate files which the operating system has to load, the more seeking across the hard drive is required, and therefore overall performance takes a hit. and then later
Another reason for Windows Vista's performance issues is the way in which Microsoft approached backwards compatibility in Vista. The operating system stores multiple copies of core system libraries, as each revision of a library typically adds/removes functions, and applications compiled with dynamic links to a specific version of a DLL file may call on functions not present in the currently installed library. So, apparently, Vista being slow is all the fault of the EU and the DOJ asking for a more modular design that didn't have everything tied into monolithic core systems. The thing is, unless I missed something, most Linux and *BSD already have exactly what is described: a very modular system with literally hundreds (if not thousands) of shared library files; moreover, versioned shared libraries have been around for a very long time as well. If having to split things out into many library files, and keep multiple versions around is such a death knell for performance, then surely something like GNOME would absolutely crawl. For those who say GNOME does crawl, note that, in comparison to Vista on the same hardware it flies -- it's only in comparison to to other lighter linux options that it looks slow. So I have to say, I'm just not buying the excuse. Modular functionality in lots of versioned library files shouldn't be a problem. I suspect it has more to do with blaming poor performance on EU anti-trust regulations than reality.
I'm fortunate to live in an area where there are *two* competing monolithic ISP's, but if they happened to both engage in these practices I'd be hooped. Here in Ottawa I have several ISPs to choose from, which includes NCF, a local cooperative that are much cheaper and have much better service and support for real problems (as opposed to the great support for only trivial issues that big ISPs have). The problem, of course, is that NCF delivers ADSL, and they get that by leasing from, you guessed it, Bell. Indeed, all the ADSL ISPs here lease from Bell, so if Bell is doing throttling, despite my apparent choice, I actually have almost none. The only other option is to lump for cable internet with Rogers -- which isn't really a choice given how badly Rogers sucks -- and I'm betting they do throttling as well. So no choice at all.
E.g., let's say we write a massively multi-threaded shooter game....Debugging it gets even funnier, since some race conditions can happen once a year on one computer configuration, but every 5 minutes on some hapless user's. Most will not even happen while you're single-stepping through the program Well that just says that you're doing it wrong. Sure, a massively concurrent system done in the manner you describe would be incredibly tricky to make work correctly. Of course that's not the only way to do it. With a little bit of thought and analysis going in you can write massively concurrent multi player games that just work right first time. That's a system that had literally thousands of concurrent processes all interacting, with no deadlock or livelock, and no complex debugging to ensure that was the case. Just because you can't imagine how it could be done doesn't mean it can't be.
I've taken a course on this in university. The tools I remember did basically an exhaustive search of all states in your program, and verified that there were no deadlocks and the properties you specified hold in every state.
Needless to say, this is very memory consuming, and can take a long time. So what you really get to verify is simple models, not your actual application with all its different variables. Also, the tools didn't grok Real World programming languages, so you had to write your model in a language other than the one you would eventually write your application in. I can't comment as to what the OP does, but these days there are tools out there that will do the job fairly well. The tools I have in mind tend to sacrifice a little bit of certainty for a healthy dose of speed. That is, they won't guarantee that there are no errors, and they may in very odd cases, flag things that are not actually errors, but they will run fast -- taking about as long as a compile operation would -- and are quite usable on modern hardware. Don't, btw, be too disheartened by the lack of absolute guarantees; while these tools don't offer complete verification, their weakness is more theoretical: they catch many many errors (on par with unit testing for rigour, though often catching different kinds of errors) very efficiently.
As to the question of whether the tools grok Real World programming languages; the ones I'm thinming of certainly do. Usually they take a Real World programming language and extend it with annotations specifying behaviour, and then verify the actual code against the specification annotations.
That means that you can write Java, annotate your with JML and have tools like ESC/Java2 do verification of the exact Java code you are about to compile against the specifications provided by the annotations. Note that you can get Eclipse plugins to integrate the extended checking right into your Eclipse session.
Alternatively, you can write C# and mark it up according to the extended language Spec#, and have a theorem prover verifying your C# code against the Spec# verifications (which are just part of the code really) as you go. This is integrated into VisualStudio; you can see an early version of this at work from 2006 here.
If you're willing to get a little more out there for Real World programming langauges, you also have the otion of using Eiffel with ESpec to provide an integrated workbench of theorem proving, automated unit testing, and acceptance testing in one package. There's also the option of going with Ada and using SPARK; in this case you have to use a restricted subset of the full Ada language, but in return SPARK provides real soundness guarantees.
So I guess the answer is: yes, there are real tools that make this sort of approach practical and integrate well with Real World languages.
I too know how to verify a program but it is no panacea. For most (non -safety critical) applications, it is too labor intensive to be used. Would you use verification to create a game? Absolutely not! However, if you are software for the avionics of a plane are the software on a medical respirator, you would use it. It's all a balance between cost and reliability. There are plenty of halfway houses though. There's lightweight formal methods, which tradeoff complete guarantees of soundness for fast an automated static checking that is still far more rigorous than anything most compilers offer (indeed, it is more on par with unit testing, but can catch different kinds of errors). There's also the option of being more rigorous only where it is needed. It would be silly, for instance, to use formal verification for all of Microsoft Office; it's just to big, and there are too many new features getting crammed in regularly. On the other hand, it might still be very useful to formally verify various parts; for instance it might be good to formally verify all the code for calculations in Excel so that it didn't do something silly like display 100,000 instead of 65536. Personally I'd also be keen to verify that writes to files are suitably atomic, so you can guarantee that, even in the event of a crash, Word documents and Excel spreadsheets will not get corrupted.
In short, there's a sliding scale here, and it is easy enough to verify to the quality you need, and only verify as much as you require. That makes it worthwhile for a whole lot more projects than just avionics and medical software.
The point is, verification does not have to be perfect to be better than unit testing. It simply has to find more defects faster. I would go even further, and say that it doesn't even need to be better than unit testing, it just has to be able catch different classes of problems better. Verification isn't (or shouldn't be) a replacement for unit testing, but rather a useful supplement (or unit testing is stilla useful supplement to verification, depending on your point of view). If it catches some errors faster then it's worth using just to weed out those errors earlier. Done right (with appropriate tool support) verification sits alongside unit testing extremely well. What can be stated easily as a specification can be done so: you can apply theorem provers to it, automatically generate unit tests from it, and not have to worry about your API documentation falling out of date because it will be generated from the specification along with those unit tests. For everything else you can write unit tests. None of this is hard once you have learned some specification languages, and the tool support for it (from JML and associated eclipse plugins, to ESpec, to Spec# and associated tools, to SPARK, to just various tools for Z) are getting better every day.
Just to make this a little more clear for the practical minded: the end result can be learning JML, a language that allows for annotations to Java (such as pre- and post-conditions for methods, assignability clauses for private variables, etc.). What benefit does that get you? Well you can use ESC/Java2 to run a theorem prover over those assertions about how things are supposed to work to verify that you code will actually meet all the claims you make of it (which is great for catching subtle unlooked for conrner cases). You can use the jmlunit tool from JML itself to create an automated set of unit tests to exercise you code against your annotations, and you also get (via jmldoc) to have your requirement annotations automatically included in your javadoc api documentation. When you consider that, for a lot of code, you ought to be writing those methods requirements up in api documentation anyway, all the extra extremely rigorous (and static/compile time) checking is just gravy. So there is plenty of practical benefit that's easy to get. To make best use of it, of course, you do need to have some grounding in how this sort of thing works so you can write your specifications well (no different, in many ways, than having some grounding in how CPUs work so you can write more efficient code).
Well the Clay Mathematics Institute is currently offering seven figure sums for seven different math problems. I can't say that much of a dent has been made on most of those problems. In fact the only solved problem had the solver (Perelman) turn down the cash. Perhaps $1 million isn't enough -- compared to the prize for solving the longitude problem, adjusted for inflation, it's pretty small. Perhaps we should be talking about 8 figure sums? If we can pay an actor $20 million dollars to appear in a film, is it really that bad to pay a researcher (or team of researchers) $20 million for solving the Hodge conjecture, or proving P!=NP?
Moral of the story... oppressive censorship, iron-handed dictatorship, and state sanctioned murder/torture are okay as long as the United States disagrees with your ideology. I'm pretty sure that's not at all what he said. An explanation of why something is the way it is is not codoning nor excusing the state of things. I'm constantly surprised by the number of people who can't seem to read or hear an explanation regarding why something terrible has happened without assuming it is an attempt to excuse the atrocity. Is a little bit of nuance and slightly more than pure black and white that hard to come by? It is possible to look at more complex explanations and motivations than just "the people who did it are evil" without saying that nothing evil happened, nor that the people who did it don't still bear responsibility.
I think that raises another point about Ghosts that has been largely missed: this isn't an otherwise terribly marketable album, at least not from a label perspective. It's 36 varied purely instrumental tracks with no catchy singles, no hooks, and nothing ideal for radio play. If Trent had handed this to a major label they would probably have just quietly buried it. Yes, there are niche labels for this kind of material out there (Warp being the most prominent that comes to mind), but they don't exactly have major marketing budgets. I suspect Ghosts will get far more listeners who weren't already fans going this route.
Kate is a much better editor than either vim (stateful editor? No thanks!) or emacs (ever tried to get line numbers on that thing?) Yeah, I have tried to display line numbers. Quite easy with this. It's a rare case where I would want line numbers of course -- the currne tline number is in the modeline, and going to a given line number is straightforward, so displaying them usually doesn't matter.
Let's assume that you have the magic Star Trek matter replicator and can make a copy of the car, although it is true that you haven't deprived the owner of the car, you have deprived the manufacturer of the car. Car manufacturers do not charge the sum of the input resources; they charge extra in order to recoup the value of their design, the costs of building the factory and yes, a profit; so if you could replicate the car you have pretty much the precise analogy of copying/sharing a copyrighted item - There has clearly been a financial impact to the car manufacturer. Indeed it would have an impact on the manufacturer. I think, however, that the real question is: faced with the ability to just replicate as many cars as we desired, and the potential for everyone who wanted a car to have one at essentially no cost, should we:
Ban replicating devices and make it illegal to copy cars;
Celebrate the fact that everyone is now wealthier and can have a car, and set to work on figuring out a way to ensure car designers still recieve suitable encouragement to design and build prototypes.
I can acccept that, with option 2, it may be reasonable to keep restraints in place until a suitable system to reward designers has been hammered out and put into place; but that's only an interrim solution, and we really should be investing a great deal of energy in getting that sorted out so we can let everyone who wants a car have one.
It really doesn't require "hopeful monsters", with a brand new species being born in one generation. All you need to do is separate a population, and let them breed amongst themselves for a while. The isolated population can remain internally compatible (i.e. able to breed with one another) while developing external incompatabilities (becoming unable to breed with their "cousins" elsewhere).
For an extremely simple example of how such an incompatability can develop, you only need two mutations. The first is completely neutral with regard to compatability (but potentially provides other advantages for the isolated population). Once that mutation spreads (over many generations) to the point where it is fixed in the population, along comes mutation number two, which is neutral for compatability for carriers of mutation one, but results in dead offspring if a carrier of mutation two breeds with an individual that doesn't carry mutation one. Once mutation two spreads throughout the isolated population, we have a group that can no longer successfully breed with their "cousins" abroad: they are genetically incompatible with them since outside of the isolated poplation mutation one either didn't occur, or never spread (i.e. didn't provide advantages outside of the isolated environment).
That's of course the simplest two step process, but you cna easily have more complex sequences of mutations, all interdependent with a great deal more subtlety in play, that give rise to genetic incompatability between populations in a similar way.
Oh I didn't say it wasn't musically interesting, just that I (being a mathematician and not a musician) am probably not the best person to judge the musical quality. From the mathematial point of view, however, it provides a very elegant and deep mathematical framework from which to build a theory of composition and a theory of performance. DO these theories, put into practice produce great music? Well it sounds good to me, but then I'm hardly a good judge... and that was all I was saying.
For an interesting take on mathematical analysis of music, you could try The Topos of Music. It sets out to apply deep modern mathematics to issues of musical composition. Starting with a base in category theory and topos theory (hence the title), it can then spiral down to using differential geometry and algebraic geometry. Personally I don't know enough music theory to know if it really stacks up, but it is certainly mathematically very interesting (and goes well beyond the basic mathematical dabbling of some approaches to bringing math into music that I've seen).
Personally I rather some of the work by artist Benar Venet, in which equations and commutative diagrams are rendered as wall sized paintings. They can be surprisingly striking and beautiful. Unfortunately the website is flash, so I can't link directly to examples; you can find them under "Painting->Wall paintings".
It waters down the definition in the sense that any one person can self describe themselves as a member of probably at least 20 different religions. It doesn't really mean much anymore, and certainly isn't what most people associate with the term religion.
I haven't seen pure science....For every paper pointing me to this or that cause of global warming, there's another creditable paper saying the opposite or saying it's inconclusive. Mostly that says you haven't actually looked at the science, and the associated papers. For a good start, try working through the IPCC fourth assessment report WGI which is filled with a great deal solid science. Of course it is ultimately just a summary of published papers, so once you're done there you can follow the detailed references to the original papers involved (of which there are hundreds). If you can a creditable paper with a solid counterargument for each and every paper referenced in the FAR I will be very impressed.
Sure, there's plenty of politics and hype, but feel free to ignore all of that and actually go and look at the science. Once you actually get down to brass tacks and start reading the original papers you'll quickly find that there is quite a lot of solid science on one side, and not an awful lot on the other. Don't take my word for it though; actually knuckle down and read the science rather than listening to opinions. It makes all the difference.
Still, I have to argue here that there still is a "religion" of atheism, complete with "prophets/oracles", "priests", "congregations", "sacred literature" and other trappings of religion. Well if you like you can make that sort of claim; in practice you've simply watered down the definition of religion to "belief" and you can taljk about the religion of Subway (with Jared as prophet, subway advertising and brochures as literature, and people who get together to eat at subwayt as congregations), or Starbucks, or Nike, or, well, anythign that people buy into in any measure. So yes, if you like atheism is still a religion, but only in using a sense of religion that makes it all but meaningless.
I hope this will help push the use of formal methods, particularly in software development. Sadly, I doubt it. Just read the comments here, or on any other similar article on Slashdot. There are a great many would be programmers who proudly reject any sense of formality. In discussions on Slashdot I've had a a hard enough time pitching lightweight formal methods with JML or similar. I don't quite fully understand where the resistance comes from, but it is very firmly ingrained.
The program became little more than a different expression of the formal specifications, such that it would be possible not only to check that a program had no "errors" and followed the specification exactly, but it would also be possible to have an automated process translate the formal specification into a program directly. That depends on the problem. I can specify a square root finding algorithm: the output multiplied by itself must be equal to the input (within some epsilon error tolerance). I doubt you can extract any useful implementation from that. A slightly more complicated example, I can specify a sorting algorithm: the output must have all the same elements as the input, and for each index i of the ouput the ith element must be less than the (i+1)th element. Trying to translate that (or its more formal equivalent) into a program directly will get you bogosort at best. Specification can be, and usually are, considerably shorter than implementations; this is particularly true wen you start specifying code that is more than just a set of business rules.
Do you not know what Nokia does?...You better learn about the company you think only makes cellphones. Personally I quite like their rubber boots. I'm not sure if they still make them though:-(
Their methods of induction/indoctrination for new recruits are very similar, and they have a similar policy towards criticism, but beyond that I don't think there are any connections. Who knows though, maybe the creator of Landmark saw scientology and realised they were on to a good racket. Landmark can appear awfully like rebranded scientology where the science-fiction has been replaced with generic "spiritual" psychobabble.
Prior to showing your students the wonderful world of high level and interpreted languages, they should learn whats acutally going on, what exactly they are doing and what happens behind the scenes when they hit 'compile'. Indeed, and prior to showing your students the wonderful world of basic arithmetic, they should learn axiomatic set theory* and first order predicate logic so they know what's actually going on, what exactly they are doing and what happens behind the scenes when actually perform an addition.
Or, you can realise, that for pedagogic reasons it is often better to start at a simple level that provides something concrete. Starting simple (with high level languages, or basic arithmetic) doesn't mean you don't teach the deeper material -- it is still as vital as ever -- it just means you throw the students in the deep end after giving them a chance to get their toes wet first.
* If you want to be more modern (and I do) you can go for category theory and basic categorical constructions such as limits indexed over finite categories, pullbacks, (fibered) products and coproducts, adjunctions and representable functors in presheaf categories.
Slashdot Mirror
$ ls
1180
$ ls
462
Less than thousands if you rule out files that aren't shared libraries or that are just links to the same shared library; that includes the equivalents of the OS X frameworks. Note that
$ ls -R
5748
Of course the exact numbers will vary depending on what you have installed, so YMMV and all that.
Needless to say, this is very memory consuming, and can take a long time. So what you really get to verify is simple models, not your actual application with all its different variables. Also, the tools didn't grok Real World programming languages, so you had to write your model in a language other than the one you would eventually write your application in. I can't comment as to what the OP does, but these days there are tools out there that will do the job fairly well. The tools I have in mind tend to sacrifice a little bit of certainty for a healthy dose of speed. That is, they won't guarantee that there are no errors, and they may in very odd cases, flag things that are not actually errors, but they will run fast -- taking about as long as a compile operation would -- and are quite usable on modern hardware. Don't, btw, be too disheartened by the lack of absolute guarantees; while these tools don't offer complete verification, their weakness is more theoretical: they catch many many errors (on par with unit testing for rigour, though often catching different kinds of errors) very efficiently.
As to the question of whether the tools grok Real World programming languages; the ones I'm thinming of certainly do. Usually they take a Real World programming language and extend it with annotations specifying behaviour, and then verify the actual code against the specification annotations.
That means that you can write Java, annotate your with JML and have tools like ESC/Java2 do verification of the exact Java code you are about to compile against the specifications provided by the annotations. Note that you can get Eclipse plugins to integrate the extended checking right into your Eclipse session.
Alternatively, you can write C# and mark it up according to the extended language Spec#, and have a theorem prover verifying your C# code against the Spec# verifications (which are just part of the code really) as you go. This is integrated into VisualStudio; you can see an early version of this at work from 2006 here.
If you're willing to get a little more out there for Real World programming langauges, you also have the otion of using Eiffel with ESpec to provide an integrated workbench of theorem proving, automated unit testing, and acceptance testing in one package. There's also the option of going with Ada and using SPARK; in this case you have to use a restricted subset of the full Ada language, but in return SPARK provides real soundness guarantees.
So I guess the answer is: yes, there are real tools that make this sort of approach practical and integrate well with Real World languages.
In short, there's a sliding scale here, and it is easy enough to verify to the quality you need, and only verify as much as you require. That makes it worthwhile for a whole lot more projects than just avionics and medical software.
Just to make this a little more clear for the practical minded: the end result can be learning JML, a language that allows for annotations to Java (such as pre- and post-conditions for methods, assignability clauses for private variables, etc.). What benefit does that get you? Well you can use ESC/Java2 to run a theorem prover over those assertions about how things are supposed to work to verify that you code will actually meet all the claims you make of it (which is great for catching subtle unlooked for conrner cases). You can use the jmlunit tool from JML itself to create an automated set of unit tests to exercise you code against your annotations, and you also get (via jmldoc) to have your requirement annotations automatically included in your javadoc api documentation. When you consider that, for a lot of code, you ought to be writing those methods requirements up in api documentation anyway, all the extra extremely rigorous (and static/compile time) checking is just gravy. So there is plenty of practical benefit that's easy to get. To make best use of it, of course, you do need to have some grounding in how this sort of thing works so you can write your specifications well (no different, in many ways, than having some grounding in how CPUs work so you can write more efficient code).
Well the Clay Mathematics Institute is currently offering seven figure sums for seven different math problems. I can't say that much of a dent has been made on most of those problems. In fact the only solved problem had the solver (Perelman) turn down the cash. Perhaps $1 million isn't enough -- compared to the prize for solving the longitude problem, adjusted for inflation, it's pretty small. Perhaps we should be talking about 8 figure sums? If we can pay an actor $20 million dollars to appear in a film, is it really that bad to pay a researcher (or team of researchers) $20 million for solving the Hodge conjecture, or proving P!=NP?
I think that raises another point about Ghosts that has been largely missed: this isn't an otherwise terribly marketable album, at least not from a label perspective. It's 36 varied purely instrumental tracks with no catchy singles, no hooks, and nothing ideal for radio play. If Trent had handed this to a major label they would probably have just quietly buried it. Yes, there are niche labels for this kind of material out there (Warp being the most prominent that comes to mind), but they don't exactly have major marketing budgets. I suspect Ghosts will get far more listeners who weren't already fans going this route.
- Ban replicating devices and make it illegal to copy cars;
- Celebrate the fact that everyone is now wealthier and can have a car, and set to work on figuring out a way to ensure car designers still recieve suitable encouragement to design and build prototypes.
I can acccept that, with option 2, it may be reasonable to keep restraints in place until a suitable system to reward designers has been hammered out and put into place; but that's only an interrim solution, and we really should be investing a great deal of energy in getting that sorted out so we can let everyone who wants a car have one.It really doesn't require "hopeful monsters", with a brand new species being born in one generation. All you need to do is separate a population, and let them breed amongst themselves for a while. The isolated population can remain internally compatible (i.e. able to breed with one another) while developing external incompatabilities (becoming unable to breed with their "cousins" elsewhere).
For an extremely simple example of how such an incompatability can develop, you only need two mutations. The first is completely neutral with regard to compatability (but potentially provides other advantages for the isolated population). Once that mutation spreads (over many generations) to the point where it is fixed in the population, along comes mutation number two, which is neutral for compatability for carriers of mutation one, but results in dead offspring if a carrier of mutation two breeds with an individual that doesn't carry mutation one. Once mutation two spreads throughout the isolated population, we have a group that can no longer successfully breed with their "cousins" abroad: they are genetically incompatible with them since outside of the isolated poplation mutation one either didn't occur, or never spread (i.e. didn't provide advantages outside of the isolated environment).
That's of course the simplest two step process, but you cna easily have more complex sequences of mutations, all interdependent with a great deal more subtlety in play, that give rise to genetic incompatability between populations in a similar way.
Oh I didn't say it wasn't musically interesting, just that I (being a mathematician and not a musician) am probably not the best person to judge the musical quality. From the mathematial point of view, however, it provides a very elegant and deep mathematical framework from which to build a theory of composition and a theory of performance. DO these theories, put into practice produce great music? Well it sounds good to me, but then I'm hardly a good judge... and that was all I was saying.
For an interesting take on mathematical analysis of music, you could try The Topos of Music. It sets out to apply deep modern mathematics to issues of musical composition. Starting with a base in category theory and topos theory (hence the title), it can then spiral down to using differential geometry and algebraic geometry. Personally I don't know enough music theory to know if it really stacks up, but it is certainly mathematically very interesting (and goes well beyond the basic mathematical dabbling of some approaches to bringing math into music that I've seen).
Personally I rather some of the work by artist Benar Venet, in which equations and commutative diagrams are rendered as wall sized paintings. They can be surprisingly striking and beautiful. Unfortunately the website is flash, so I can't link directly to examples; you can find them under "Painting->Wall paintings".
It waters down the definition in the sense that any one person can self describe themselves as a member of probably at least 20 different religions. It doesn't really mean much anymore, and certainly isn't what most people associate with the term religion.
Sure, there's plenty of politics and hype, but feel free to ignore all of that and actually go and look at the science. Once you actually get down to brass tacks and start reading the original papers you'll quickly find that there is quite a lot of solid science on one side, and not an awful lot on the other. Don't take my word for it though; actually knuckle down and read the science rather than listening to opinions. It makes all the difference.
Their methods of induction/indoctrination for new recruits are very similar, and they have a similar policy towards criticism, but beyond that I don't think there are any connections. Who knows though, maybe the creator of Landmark saw scientology and realised they were on to a good racket. Landmark can appear awfully like rebranded scientology where the science-fiction has been replaced with generic "spiritual" psychobabble.
Or, you can realise, that for pedagogic reasons it is often better to start at a simple level that provides something concrete. Starting simple (with high level languages, or basic arithmetic) doesn't mean you don't teach the deeper material -- it is still as vital as ever -- it just means you throw the students in the deep end after giving them a chance to get their toes wet first.
* If you want to be more modern (and I do) you can go for category theory and basic categorical constructions such as limits indexed over finite categories, pullbacks, (fibered) products and coproducts, adjunctions and representable functors in presheaf categories.