Linux convergence? I’m hoping for it!

UPDATE: This has now happened!


Bought myself a nice 5.1 speaker system a few months ago – so I don’t use our tinny crappy old computer speakers any more, yay! But the irony is, I usually just plug my Nexus 7 into it (using the bog standard noisey stereo input, instead of the higher quality digital input cable) to play music from Spotify!

That’s because, while Spotify is available for Linux, it’s only officially supported at the moment on Android, and it’s been a bit of a pain to install on Fedora Linux / QubesOS – there are two community-created install methods, one of which is currently known to be broken, and neither of which worked for me the last time I tried them.

I only use Skype on my Nexus too, for a similar reason. Skype on Linux is behind – it doesn’t support group calls. Microsoft, who acquired Skype Technologies in 2011, have said they are working on it. Microsoft? Working on commercial software for desktop Linux? That’s a new one on me!

But the irony is, both Fedora and Android are Linux!

tux_in_android_robot_costume_1_by_whidden-d3aq9i2

Well, they’re Linux underneath – the operating system infrastructure on top of the Linux kernel, and how developers typically write applications, is quite different in each. There are now two main branches of Linux in the wild: desktop/server Linux, which is further subdivided into numerous distributions, and Android. “Server Linux” is conceptually just Desktop Linux with bits removed (and/or left unused) – it’s not really a separate thing, except for marketing purposes. There’s also a couple more branches of Linux which have just started to appear in the mobile market: Firefox OS and Sailfish OS; and two more nascent ones which haven’t been commercially released on real devices yet: Ubuntu Touch and Tizen.

In terms of open source, my sense is that desktop Linux and Firefox OS are the most open, and Tizen (if it ever gets properly released), followed by Sailfish OS, will be the least open, with Android somewhere in the middle in practice, although I may be wrong on that. I’m talking about the platforms here, not third-party apps – the open source application ecosystem seems to me to be far stronger on desktop and server Linux than on Android.

One of these is not like the others, though! Ubuntu Touch is an attempt to bring Ubuntu to mobile platforms – a bit like Microsoft’s ideas of platform convergence that it tried to force onto its users (not entirely successfully!) with Windows 8 – so it’s not a clean break like the other mobile operating systems.1 Sailfish also runs Android apps, but since they’re both mobile platforms at the moment, that’s not as interesting or impressive to me as the idea of Ubuntu Touch.

Also, Firefox OS is pushing the concept of HTML5 apps – although these can also be downloaded like regular mobile apps, so it’s not completely clear to me where Firefox OS really stands in the convergence spectrum.2 Sailfish also pushes HTML5, although not to the extent that Firefox OS does.

Finally – and perhaps most importantly – as I posted about yesterday on Google+, Google has said that Chromebooks will get the ability to run Android apps 3 Presumably, this means without using an Android emulator – which is slow, as far as I know. by the end of this year – and Chromium OS, on which Chrome OS is closely based, is open source. So hopefully that ability will appear in Chromium OS, and then be ported to other Linux distributions – solving my Skype and Spotify dilemma.

A Samsung Chromebook. Photo by Alex Washburn/Wired [CC-BY-1.0 (http://creativecommons.org/licenses/by/1.0)], via Wikimedia Commons

The music industry probably won’t be bothered, as they’ve already agreed that Spotify users on tablets can have the same rights to stream music as Spotify on desktops – unlike Spotify users on mobile phones.4 But how do phablets fit into Spotify’s streaming licensing scheme? We simply must be told!

But goodness knows what Microsoft will make of that! Wailing and gnashing of teeth, probably!

Footnotes

1.
 Sailfish also runs Android apps, but since they’re both mobile platforms at the moment, that’s not as interesting or impressive to me as the idea of Ubuntu Touch.
2.
 Sailfish also pushes HTML5, although not to the extent that Firefox OS does.
3.
 Presumably, this means without using an Android emulator – which is slow, as far as I know.
4.
 But how do phablets fit into Spotify’s streaming licensing scheme? We simply must be told!
Tweet about this on TwitterShare on RedditShare on FacebookShare on Google+Share on TumblrShare on LinkedInPin on PinterestShare on StumbleUponEmail this to someonePrint this page

A modest proposal

I made this fun presentation on how to simultaneously solve the Eurozone crisis and political bribery (inasmuch as the latter significantly affects the population at large).

Performance-Related Politics

Tweet about this on TwitterShare on RedditShare on FacebookShare on Google+Share on TumblrShare on LinkedInPin on PinterestShare on StumbleUponEmail this to someonePrint this page

Things not to take literally: “What do you care what other people think?”

Trigger Warning: General

What Do You Care What Other People Think: Further Adventures of a Curious Character is the title of an autobiographical book by physicist Richard Feynman. He was indeed quite a character, so one might reasonably suppose that he felt the former sentiment applied to him, and that’s why he chose it as the title of his book. (I highly recommend his series of autobiographical books, by the way, they’re funny, engaging and I think most intelligent people would enjoy them – except that if you are anti-nuclear-weapons you might not like his views on those, which are in a very real sense a product of his time and of his working on the Manhattan project. Likewise with his attitude to women I suppose, although I wasn’t as sensitive to that – certainly not when I read the books as a teenage boy, anyway.)

I think it’s important, especially if you are the sort of person who might take “What do you care what other people think?” too literally at least sometimes, not to take this idea too literally. Or to put that another way, not to take it to extremes.

Now, I’m going to do the standard thing of ignoring what the writer actually meant – because it’s a common enough sentiment in Western society, after all – Richard Feynman’s ghost can’t lay exclusive claim to it or anything.

I think it’s helpful to see it as a genuine question, as a starting point for reflection on whether what other people might think actually matters to you and why. So in that sense, do take it literally – as a literal question, not merely a rhetorical one. I don’t think it should be seen as a command or guidance to just simply ignore what other people might think, because it’s somehow “manly” or “brave” or “hipsterish” or “idiosyncratic” or “anarchist” or whatever else it might be that you want to be, or think you are. (I’ve certainly never thought of myself as an anarchist, at least, but I put that one in there because I think it is highly relevant to people in radical milieux, for fairly obvious reasons).

And certainly it should not be seen as applying in all contexts, in all social situations, with equal vigour.

Yes, not for the first time, this blog post is partly aimed at myself – but also to anyone else who might be a bit overzealous about “not caring what other people think”. Oh, I know I’m not the only one.

One example of where I think this sentiment really has value, is supporting someone who wants to “break the mould” socially in some positive or (you think) legitimate way, and is actually aware of the potential social costs of doing so and what that could entail, so they’re attempting to be brave in full (or at least partial) knowledge of what they could be getting into, and not just foolhardy.

One example of where this sentiment could be harmful, is if it leads you to ride roughshod over other people’s feelings. To take one extreme – but therefore compelling – example, if someone is a survivor of childhood sexual abuse (and remember you don’t actually know if any of the people in your social circles actually are survivors, but haven’t chosen to tell you), they may be particularly sensitive to all sorts of things – words, concepts, expectations, even just their perceptions of what you are implying or what you expect – that you’re perhaps not fully aware of.

Yes, it’s hard to guarantee (well, impossible to guarantee 100%) that you won’t offend. But, life is hard, and remember, if, like me, you’re not such a person yourself, it’s especially hard for them. So have some empathy. One thing that might help a little bit, is writing Trigger Warning (or TW for short, useful on a tweet), which can act to give such people a choice to avoid things that may trigger traumatic memories and/or make them highly emotional. Which is what I’ve done on this blog post.

Now, that’s just one example. I don’t mean to imply that that’s the only context in which you shouldn’t thoughtlessly ride roughshod over other people’s feelings (and, as I said, you can’t ever know for sure that you’re not in that particular context anyway).

It’s often been observed, in as many words, that it’s easier to ride roughshod over other people’s feelings online (I’m not going to link to the coarse version of this that is initialled GIFW, just because I personally choose not to swear very much online). Some of the reasons for this are obvious: for starters, no facial expressions or other body language (unless you’re on a Google+ Hangout or something video-based like that), so we don’t get the same social cues, and as a result it can be necessary for people to be more blunt to us to get through to us, than they would have to be in offline interactions. Well, maybe you’re really really good at online interactions and never need body language to interpret how someone is feeling. I would seriously question that idea, however! Not least because they may not want to show you how they are feeling when discussing something online, for various reasons!

Finally, it’s also worth asking yourself, if you are tempted to follow the principle “What do you care what other people think?”, whether you aren’t simply “not caring” about one group of people’s feelings, in order to “look good” or “look cool” or bond socially with the person or people who have just told you or suggested to you not to care what other people think – and therefore, you are in fact caring a great deal about what that second person or group of people think? Not that there’s necessarily anything wrong with that! But is there some in-group versus out-group effect going on here? Obviously, it’s perfectly commonplace for people to think in terms of in-group and out-groups – it’s probably part of our shared evolutionary psychology as a species, but…

No links because this post is long enough already. See, I’m thinking of you, the reader!

Tweet about this on TwitterShare on RedditShare on FacebookShare on Google+Share on TumblrShare on LinkedInPin on PinterestShare on StumbleUponEmail this to someonePrint this page

Women in computing – an apology

In which Robin actually learns something important.

Recently, a professor made an ill-judged remark about women at a conference about the Haskell programming language. Tim Chevalier blogged a criticism of the comment as sexist and off-putting to women thinking of going into Haskell or computing. That was when I made a stupid mistake. I tweeted to Tim that I thought the professor’s comment was “acceptable”, and then debated the issue and follow-on issues for several days online on Twitter and Reddit, before finally realising I had to write this blog post. (Tim has since posted a much longer version which I think is much better, so if you saw the first blog post and, like me, weren’t totally convinced, go read that one. You really should, if you are such a person, on both moral and pragmatic grounds! And try not to let anything which may seem too strident or comments which you may strongly disagree with, detract from keeping in mind the original complaint, which is perfectly sound, as I’ll argue below.)

Why did it take so long? Well, part of the reason is to do with the fact that I am a member of a group – which is to say, men, or to put it perhaps more accurately, white Western adults, or perhaps it would be even better to say human beings – which has a tendency to solidify and double down on their views in the face of criticism that they initially perceive as unjustified, highly abrasive, or ganging-up. That is not to say that they were necessarily unjustified, just that at the time, I perceived some of them as such. Another reason is that I have a job in the private sector and wasn’t particularly motivated to read what I just thought would be “more of the same, albeit possibly more radical”, in what little time I had left after spending time with my wife, reading and replying to tweets and reading and replying to reddit comments. Yet another reason is that I didn’t agree with everything that was said in the ensuing discussions (see the end of this post for an attempt at conciliation).

And psychologically, it’s sometimes much easier to blame and rail against others, even if those complaints may happen to be tangential, than to accept that you might have been wrong, in a morally significant way. Come on, don’t say you haven’t been there. We’ve all been there, haven’t we?

Of course, these tendencies – and indeed many of the abstract argumentative tropes that can be identified in the arguments that result – are not specific to discussions about feminism! They are general issues that occur in all sorts of human interactions, especially domestic ones, where you can’t just instantly block someone like you can on Twitter. Well, you can at least request a cooling-off period, which may be a good idea in such a situation.

Anyway.

The (apparently) offhand comment the professor made was unacceptable not only for the obvious reason that it did actually offend some women – and as I said myself during the course of the Twitter discussion I was involved in, women get to define what is sexist, not men. This should be enough – fundamentally, in a sense, you can stop reading right there. But if you want to read on: It was also unacceptable because:

  1. Anyone who supervises PhD students, as a professor does, is probably going to be supervising them directly for three or four years, or even more. Also, PhD students don’t receive a lot of money (on the grounds that they are undertaking a course of study from which they will benefit rather than doing a job), and they do have the option of applying for a job in industry instead. It is therefore incumbent on PhD supervisors not to drive away potential students with unwise remarks, and not to start the supervisory relationship on the wrong footing by saying anything that could lead to a suspicion that “This is a creepy person who says or thinks things like this all the time.” The latter is sadly not unheard of in academia. Now, before any sceptics of feminism get angry at me, I’m not making the claim (which would be totally ridiculous, especially coming from me) that there’s something wrong with being sexually attracted to women. There is a distinction to be drawn between being appreciative of the opposite or indeed same sex, and behaving in a way which is widely viewed as creepy or taking advantage of your students.
  2. Professors have an obligation to set a good example, to more junior staff and to students, of how to behave professionally and how to market the university environment appropriately. I don’t think this is controversial at all, as a general principle of conduct. (I don’t at all mean to imply that professors should not criticise the university environment, of course – that would be a grave encroachment upon academic freedom – only that if they intend to market the university environment, they should on pragmatic grounds take into account how their comments are likely to be received.)

Points 1 and 2 would probably have been obvious, perhaps too obvious or even secondary to consider mentioning, to many women encountering the professor’s comments. But personally, as a no doubt fairly typical man, never having been the target of sexual harassment or inappropriate sexual comments from an authority figure, they didn’t occur to me in the initial heat of the moment, when – as I’ve already said – I posted a stupid tweet.

You can find more arguments in the Reddit comments for the original blog post. I wouldn’t want anyone to come away from this without realising the Haskell community had strongly publicly disapproved of these remarks, albeit belatedly. For which we, or rather they (because I’m not really actively part of the Haskell community at the moment) have Tim to thank.

I would therefore like to take this opportunity to apologise to anyone affected by sexism who was offended by that particular hasty, thoughtless tweet of mine. I’m sorry. And I won’t claim that any statement relating specifically to women is “acceptable” or “OK to say” or anything like that without first listening to those who it affects, again. And if I ever do, you have my full permission to admonish me and mention this very blog post right away. Because, that would be hypocritical of me, and I don’t actually want to be a hypocrite, nor to morally go backwards. Indeed, I want to morally go forwards. Shouldn’t we all want that – those of us who have some time in our lives to think about self-improvement and who aren’t moral saints, at least? (Anyone who thinks I shouldn’t have apologised, should think about that previous question.)

This series of events has also caused me to reassess my general attitude of “just go ahead and tweet it, you can clarify or discuss or retract later if needed”. (An attitude which may have been influenced by (a) an acquaintance I respect who advised me not to care about offending people on Twitter, (b) a male feminist who strongly implied to me that it was actually patronising to withhold a tweet because it might offend someone.) I thought of bleating that this thoughtlessness was uncharacteristic of me, but unfortunately of late it actually isn’t. Just because you only have 140 characters, doesn’t mean you have to spend 140 milliseconds thinking about a tweet before writing it. That doesn’t mean that you have to ponder onerously every retweet of a kitten picture, but… just remember the internet really is serious business sometimes (no joke). Yes, I am talking to myself, thanks for asking – but also to anyone else who is a bit like me who may be reading this.

So, as a man who at some point in time had an incorrect opinion, I obviously had a choice. I didn’t need to push my ill-founded opinion out there assertively and wait to be educated – as if this was some high-school debating society – I could have waited for it to happen naturally. That might not have happened any time soon had I ignored the discussion entirely (side note: in many things, such as online polls, we forget about all the people who don’t participate or don’t notice and we get a biased perception of reality as a result), but one good way to stimulate discussion about something is to submit a blog post to a relevant, active subreddit on Reddit and then come back and read the discussion later – ideally at least 24 hours later. It’s a bit hit and miss, especially these days, but out-of-the-ordinary / controversial things are good to spark discussion.

All that said, I would like to re-emphasise my call for us all to look for and support or engage in diverse approaches towards trying to increase the number of women – and people generally – in IT, based on learning about and understanding the multiple and varied reasons why many women (and many people generally) don’t end up in IT, or don’t stay in IT when they get there. That is, it’s not all about off-colour remarks like this in the adult world – it also has to do with issues occurring much earlier, attitudes and preferences of teenage girls, and so on. I’ll stop there, before I offend anyone again.

Comments welcome, but comments that make me go “OMG, how could you say that!” may be deleted.

Tweet about this on TwitterShare on RedditShare on FacebookShare on Google+Share on TumblrShare on LinkedInPin on PinterestShare on StumbleUponEmail this to someonePrint this page

Why Kubuntu is not ready for the desktop

It’s great that Kubuntu allows you to report bugs direct from the desktop, but this doesn’t work at all. In my experience, every single aspect of it, just doesn’t work. I don’t know how many of these problems are general Ubuntu problems, and how many of them are specific to Kubuntu or KDE or Qt or my graphics drivers or the phase of the moon. All I know is that they’re problems.

(Note: This story is actually a hybrid of two true stories, to make it sound even more impressively bad. Most, if not all of it, could have happened this way, but it didn’t.)

I want to report a bug in a package. I look at the apport-bug man page (I knew to look there from a few months ago when this process did sort-of work), and it tells me I should, and I quote, “always” file a bug report by just typing apport-bug with no arguments. Fine. What are all the other command-line arguments there for, then?

I type apport-bug.

Which of these problems is it? OK, it’s none of these: I choose “Other”.

It then asks me what kind of display problem it is… What?! It’s not a display problem. Not even close. I didn’t choose Display problem!

FAIL.

What do I choose now? The only thing I can rationally choose is Cancel.

But the Cancel button doesn’t work.

FAIL.

I go back to konsole (I love konsole. In recent years it just works, with no problems at all. Unlike the rest of KDE.) I try to kill apport with CTRL+C.

It doesn’t die.

I kill it with CTRL+Z and kill %1.

It finally dies.

But my problems are not over. Oh no. My problems have just begun! I foolishly decide to try again!

I look at the apport-bug man page again, and see that I can specify a PID as a command-line argument. I do so.

It tells me I’m not the owner of that process, so I need to run it as root.

Fine. I do so.

It can’t work out which package owns the program running in that process.

Fine. I guess I should have just told it that in the first place, since I knew it.

I tell it which program it is.

Finally, things seem to be working!

As rekonq is uploading the bug report, I leave it running in the background. And then it crashes. So does apport-bug. At the same time.

FAIL.

Helpfully, a wild KCrashHandler appears, and asks if I want to report this crash as a bug.

I do. (I don’t know why. I should have just given up at this point. I’ll know not to do so next time.)

I go through the KCrashHandler dialogs, mashing checkboxes and buttons, lying that I knew exactly what happened and what I was doing, until it finally haughtily deigns to admit that maybe, perhaps, my bug report is “high quality” enough to be submitted to the developers.

Then… it refuses to submit it. Because apport-kde is not covered by the Ubuntu bug-tracking system. (Or was it the KDE bug tracking system? I honestly don’t remember. And I don’t care.)

Hmmm. Fail? I dunno. Is it reasonable to suppose that if you’re offered the chance to report a bug on a bug reporting tool, that there will be some kind of … I don’t know, bug tracking system, to actually receive your report? I dunno – you tell me.

Then I click Finish and it shows me the bug report it would have submitted to the Ubuntu bug tracking system, had it been able to. Then it tries to submit it via email, using KMail.

At this point, KMail appears – and immediately crashes. But not before telling me that it has to crash now, sorry. How nice of it to let me know! Admittedly, I haven’t configured KMail at all, so there’s no reason why it should work. But there’s also no reason why it should crash at this point.

FAIL.

I write the email myself. Well, no, I lied – I copy-pasted it into GMail.

I receive an autobounce email saying I am, and I quote, “not allowed to post to this mailing list”.

It doesn’t say, “just click here to subscribe to show you’re a real person, not a spammer”. It doesn’t explain anything. It just says I’m “not allowed”.

HOW RUDE. AFTER ALL THIS EFFORT I’VE GONE TO.

I write an irate email to the owner of the mailing list, using the email address provided in the bounce email.

THE ULTIMATE FAIL: I received no reply. I suspect that the owner email address redirects to /dev/null.

At this point, I gave up. No, I lied – I wrote this blog post.

Then I gave up.

The end.

Tweet about this on TwitterShare on RedditShare on FacebookShare on Google+Share on TumblrShare on LinkedInPin on PinterestShare on StumbleUponEmail this to someonePrint this page

Getting your face to appear under Google search results linking to your blog

UPDATE: If following these instructions messes up your blog post titles, tick the checkbox “” in Settings -> Yoast SEO -> Titles & Meta’s.

This post is for fellow bloggers using WordPress.

There is a slightly pernickety list of things you need to do to get Google to realise that your Google+ profile is owned by the same person that writes your blog posts, but once you’ve done so, Google may eventually (when it next updates) choose to show your profile photo under at least some of your blog posts.

But first, a couple of disclaimers:

  • As Google says:

Note that there is no guarantee that a Rich Snippet will be shown for this page on actual search results. For more details, see the FAQ.

  • Read the last step below first – there’s a potential privacy issue

If you still want this feature, you might want to use the Yoast SEO plugin, which has a new feature which makes that slightly more convenient to set up. No need to read that post though – here are the full step-by-step instructions you need to follow, exactly as I performed them:

  1. Download the latest Yoast SEO plugin development version from this link (it’s free)
  2. In your WordPress Dashboard, go to Plugins -> Install and choose to install a plugin via a zip file
  3. Install the zip file you just downloaded in step 1
  4. Activate the plugin using the link provided
  5. On the top-right corner of the page, click “Howdy, [Your Name]” to edit your profile.
  6. You should see a new profile field at the bottom: Google+ profile page. In a new browser window or tab, go to your Google+ profile page, and copy and paste its URL into the profile field I just mentioned.
  7. Delete the /posts part at the end of the URL you just pasted (I’m not sure whether this is actually necessary, but let’s be on the safe side).
  8. Important – Click the button at the bottom to save your changes!
  9. On your dashboard sidebar you will now see a new link at the bottom – SEO. Inside there, choose the subpage “Titles and Meta’s” [sic]
  10. Click the Home tab at the top of the page (yes, it’s a settings subpage with tabs – this Yoast SEO plugin has a lot of settings!)
  11. At the bottom, choose yourself in the dropdown next to “Author highlighting”
  12. Once again, click Save Settings.
  13. On Google+, edit your profile and add a link from your profile to your blog homepage.
  14. On Google+, make your +1 tab publicly visible if it isn’t already. (This may be a privacy concern for you, in which case, bad luck – you’ll have to make the decision as to which you value more – the privacy of your +1 clicks, or this new Google search results feature.)

OK, this was still a pretty involved process. However, the Yoast SEO plugin also has a load of other goodies included – including the ability to easily stop search engines from displaying archive pages in search results, but still let them crawl through them for links. Those particular settings are a must for all WordPress bloggers – it’s just really annoying and unhelpful when date or category archives rather than the actual blog post of interest show up in Google search results. It seems like half the time, the post of interest has fallen off the end of the archive page, and isn’t even visible any more!

So it’s worth going through this rigmarole and doing it this way. Also, you don’t run the risk of screwing up the HTML/PHP and wondering what’s happened, which is good if you don’t like editing HTML or PHP.

Tweet about this on TwitterShare on RedditShare on FacebookShare on Google+Share on TumblrShare on LinkedInPin on PinterestShare on StumbleUponEmail this to someonePrint this page

Comparison of functional program verifiers

This is a comparison of various tools for “verifying” that a piece of code (written in a functional programming style) fulfils a specification, with some degree of automation, to various degrees of confidence.

I’m not putting this on Wikipedia, because many Wikipedia editors will summarily delete supposedly “non-notable” table rows in tables, despite there being no Wikipedia policy to do so.

Note: DSolve is currently not included because the published version does not support recursive types, such as List.

Basics

Name Available for download Mode(s) Solvers Operates on
Leon Yes Automated Z3 Scala
Isabelle Yes Interactive Various Various4
Coq Yes Interactive2 Built-in2 Various4
Dafny Yes Automated1 Z3 Dafny
ScalaCheck3 Yes Stochastic None – direct execution Scala / Any
HMC No Automated Various ML
ACL2 Yes Automated, stochastic Built-in ACL2

1 Dafny really shows that the lines between interactive and automated provers have blurred. It has an intriguing feature – the ability to prove lemmas by giving the solver enough hints to let it prove it by itself, and then have those lemmas be automatically employed by the solver. I am not sure whether any other system offers such a feature, as such.2

2 Coq does not yet integrate with any solvers (other than its built-in decision procedures), though a project is underway to change this. So why would you want to use Coq instead of Isabelle at the present time? Well, one possible reason is that Coq supports dependent types (although not in such a convenient way as languages specifically designed for dependently-typed programming), whereas Isabelle doesn’t.

3 ScalaCheck is one of a family of independently-developed tools named something-Check, which began with QuickCheck (which is for Haskell).

4 These tools (Coq and Isabelle) both support code extraction to proper programming languages. Alternatively, there are front-ends to both which can read e.g. Java code and specifications, and create corresponding proof obligations. So don’t worry about being able to execute your code with reasonable performance outside of the tool – you will be able to.

Features

Name Static typing Proof by induction Verifying higher-order functions Natively supports imperative code IDE
Leon Yes Yes No No No
Isabelle Yes Yes Yes No Emacs or JEdit
Coq Yes Yes Yes No1 Emacs or CoqIDE
Dafny Yes Yes ? Yes Emacs
ScalaCheck Yes No Yes Yes Any
HMC Yes ? Yes ? ?
ACL2 No Yes No No Emacs or Eclipse

1 Coq does not support imperative programming “natively”, but it can be done in Coq, using e.g. Ynot or Bedrock.

Corrections and additions can be supplied by comment below or by email; please supply a citation to a reliable source in every case.

Tweet about this on TwitterShare on RedditShare on FacebookShare on Google+Share on TumblrShare on LinkedInPin on PinterestShare on StumbleUponEmail this to someonePrint this page

Alternative currency for Scots?

Scotland is to have a referendum on regaining independence from the UK, and if the result is Yes, signs are that they are set to make the disastrous mistake of retaining a currency union with, or pegging to, Pound Sterling.

But as I often find myself saying: The Greens get it. Thank goodness someone does!

As, in fact, do Labour. It’s a wonder what needing to understand something in order to attack your political opponent can do! Suddenly the Labour Party is discovering the flaws of currency union without fiscal union that they were as a party so blind to when it came to the Euro.

Patrick Harvie has raised questions about defecting from pound sterling.

By SCOTT MACNAB
Published on Tuesday 29 May 2012 00:00

An independent Scotland will have to look at setting up its own currency, according to one of the “Yes” campaign’s leading figures

Tweet about this on TwitterShare on RedditShare on FacebookShare on Google+Share on TumblrShare on LinkedInPin on PinterestShare on StumbleUponEmail this to someonePrint this page

Nokia have good taste

Totally Enormous Extinct Dinosaurs

Tweet about this on TwitterShare on RedditShare on FacebookShare on Google+Share on TumblrShare on LinkedInPin on PinterestShare on StumbleUponEmail this to someonePrint this page

Germany seeks free money

Originally published here, with 7 comments

There are three ways for governments to get free money, without having to increase taxes. One is, of course, starting a national lottery (but there’s only so much money that can bring in). The second is by following the advice of MMT economists and creating money to fund themselves – a route open to all governments. The third way is this:

Germany Announces New Bond That Will Literally Pay You Nothing

Tweet about this on TwitterShare on RedditShare on FacebookShare on Google+Share on TumblrShare on LinkedInPin on PinterestShare on StumbleUponEmail this to someonePrint this page
this site uses the awesome footnotes Plugin