skew

It's smaller, but not actually negligible. An old but oft-cited 2002 study said a laptop with a three year lifecycle took about twice the energy to manufacture as operate. Silicon is much more energy intensive than other materials, with fab energy consumption apparently relatively steady over time on the order of 1 kwh/cm^2 of silicon processed.

So, there is a high bar for replacing a computer with a new one to actually save net resources, but an actual 10x reduction in power consumption like replacing a P4 desktop with an RPi is big enough to pay off reasonably quickly.

Interesting that you mention neutrino astronomy - if you mean imaging, I don't know of anything but gravity that could focus neutrinos.

You haven't got many fun answers yet? Here are a few nice programs

http://incredible.pm/

http://fluffynukeit.com/software/fnistash/

http://hledger.org/

If you're looking for not-necessarily-polished personal toy projects, probably just about everything in Hackage's "Game" category fits:

http://hackage.haskell.org/packages/#cat:Game

Monadius has an interesting look. Sadly a touch of bitrot since 2013 - you'd need to `cabal get monadius` and edit

    --- Monadius-0.99/src/Monadius.hs	2013-05-28 
    +++ Monadius-fix/src/Monadius.hs	2017-01-25
    @@ -18,5 +18,5 @@
     import Data.List
     import Data.Maybe
    -import Graphics.UI.GLUT hiding (position)
    +import Graphics.UI.GLUT hiding (position, DebugMessage)

Dare I hope "arguments against anthropomorphic global climate change" was not a typo? If not, please share!

Do you mean "seL4 is great"? I agree it won't do much for application-level security without adding some formally verified code on top (perhaps as simple as setting up isolation between VMs), but it looks great if you do want to use formal methods. For the simplest thing, just starting out with a formal semantics of the OS and reason to trust that semantics would save a lot of work (of course, a lot may remain).

Why do you think D-wave machines can be clustered at all? Unless you say it's operation is not essentially quantum, that would mean demonstrating coherence between a bunch of machines and a scalable quantum network!

I disagree extensively - raw data should definitely be available, and there are a number of interesting things you can do with it without any special expertise. For one, evaluating whether those adjustments even affect any overall conclusions you are concerned about, like this:

http://forums.sandiegouniontribune.com/showpost.php?p=532360...

If there is incompetence at play here, it's in failing to get ahold of raw data.

I'm sceptical that you've ever actually tried to get any data. The first sentence of NASA's GISTEMP page tells you where they get there data, and a few more clicks will get you to daily logs for a decent chunks of it.

http://www.caltech.edu/news/caltech-announces-discovery-fund...

The response to the client is only sent after a majority of followers have the log entry. That's described in the text in the "Protocol Overview", and nicely animated in "Log Replication".

Non-Turing-complete is not a bad way to go. You pretty much have to already be a researcher in dependent type systems (or maybe set theory) to invent functions that always terminate but can't be written in non-Turing-complete languages like Coq (an evaluator for programs in an at-least-as-powerful dependently typed language is the only remotely natural example I know of). Also, writing a program that proves some programs terminate is way easier than proving a program that correctly proves any terminating program terminates, if you are confusing the two. If it's not too common, "I didn't manage to prove this terminates" sounds like a reasonable compiler error.

That sounds like a pretty reasonable density to see savings in threaded forth code like the second post talks about (it also mentions adjusting the shift for other densities). Second, you don't need to reserve excess state at the end like that if the linker/compiler takes a little care allocating offsets so the last instructions use small indices. It definitely seems like a bit of a specialized trick, but the articles do a decent job describing conditions where it might make sense.

Wasn't that precisely the first complaint - observing a pair of incidents which make no sense as a consistent policy? (the second complaint being that even a senator had trouble clearing up a mistake). Both the original comment and reply are consistent with that reading.

Regarding those particular operators, + is conventionally reserved for commutative operations (e.g, http://en.wikipedia.org/wiki/Plus_and_minus_signs#Plus_sign).

"kinetic energy" means nothing alone, thrust and specific impulse are better metrics to look at. Doing a lot better than ion thrusters at either without being too much worse in the other and energy efficiency would be interesting.

However, the article quotes an exhaust velocity of 30km/s (or ISP of 3000s), and using 200kW doesn't leave much room to beat http://en.wikipedia.org/wiki/HiPEP on thrust without counting on net energy gain. The linked slides also claim net energy gain.

That's actually the only place ML^F ever requires type annotations - when you want to take a polymorphic function as argument and use it at different types. MLF is basically as strong as inference for polymorphic types gets, so it's not surprising annotations might be needed here too. (intersection types handle the example nicely, but I don't know of any languages using them).

If you want to faithfully translate the idea that 5 and "Test" are different values that can be passed into the same places but told apart by tests if you want, you might translate the second line to something like f (\x -> x) (Left 5) (Right "Test"), which does pass.

There are some nice examples of re-using the same code at successively more interesting types in Conor McBride's ICFP keynote:

http://www.youtube.com/watch?v=XGyJ519RY6Y (video only, the presentation was liveish coding in emacs and I haven't found the source files)

Agda of course pursues the anti-thesis of dynamic typing.

The previous article really didn't make the argument "all you need is static typing". It was specifically refuting the idea that "all you need is unit testing" - or at least that unit testing is a complete replacement for static types.

The paper makes a point of reporting that most unit tests could not be replaced by static types.

What of that looks like a claim that you only need types?

The first half is a bit easier - if you can show some implementation meets the specification it is at least consistent.

The second isn't so clear, but sometimes you can get a bit more confidence by showing that other good properties are implied by the specification alone.

Yes, foldr/build is almost exactly reducibles, but not foldables.

Iterators do nothing for parallelism either.

Isn't foldr/build fusion much closer? A collection is represented by a "build" function that takes the reducer, and list transformers become reducer transformers. The main difference is that it's applied automatically by list library using rewrite rules, so it's not as obvious, the reducer is supplied as a pair of "cons" function and "init" value rather than a variadic function, and there's no parallel fold.

http://research.microsoft.com/~simonpj/papers/deforestation-... The first paper (yes, that's a .ps.Z - check the date)

http://www.scs.stanford.edu/11au-cs240h/notes/omgwtfbbq.html some recent slides, which also include a bit about a "stream fusion" which isn't yet in the standard library

http://darcs.haskell.org/cgi-bin/gitweb.cgi?p=packages/base.... The details from GHC's libraries - it's all in the RULES.

The cost model can be very simple. Take the cost model of Java and apply it to programs where all fields are final. Maybe costs are higher than you'd like, but it's simple to understand.

Lazy evaluation seriously complicates the cost model, but few languages are lazy.

That's incoherent.

If you accept the claims of

> People regularly say they translated their system from language A to language B and got 10-100 times code-size reductions.

then it's clearly false at least for first systems that

> there is essential complexity in software, and it is the dominant factor.

Every language is based on a huge mass of things which might fall under "fully understanding the tool you're using". Do you have a sharper distinction separating type inference algorithms from other things like calling conventions or garbage collection algorithms that languages are presumably allowed to sweep under the rug?

Type inference in general seems particularly benign as far as black boxes go - it is somewhat user visible, but you can limit your exposure to knowing where to put explicit type annotations.

The plain Hindley-Milner type system is particularly well behaved, in that the inference algorithms for it are guaranteed to work if there is any valid way at all to assign types. Combine that with type erasure guaranteeing the exact types assigned can't affect program behavior and the details of inference are doubly encapsulated.

Did you ask your friend if it actually looked non-trivial?

If you were really pedantic, you'd make a distinction between executing beta-reductions directly, and executing them in zero time.

Here's hardware that does the first http://www.cs.york.ac.uk/fp/reduceron/

Do you ever try to understand the asymptotic performance of a program in terms of the source code, or only read compiled binaries?

You can describe the performance of a functional program in something like asymptotic number of reductions. You can write compilers that will run those programs on real hardware in time related to the performance bound you get by working in the source model. Also, perfect optimization is undecidable. So, the question is whether there are problems where you necessarily lost asymptotic performance by working with a purely functional programming language.

> You can just as easily ask what the asymptotic 'cost' of using a non-random access Turing machine is.

Precisely. For example, you can ask whether the best algorithm for some problem on a 1-tape Turing machine is asymptotically slower than the best algorithm on a 2-tape Turing machine.

Have any of these articles included hard numbers?

These slides say GPS received power is around -160dBm http://www.ima.umn.edu/talks/workshops/8-16-18.2000/van-dier...

I see unsourced claims LightSquared signals would be around -70dBm, which is at least roughly consistent with LTE.

If so, that's a signal 1,000,000,000 stronger than the satellite-to-ground signals LightSquared's band was allocated for, immediately adjacent to the GPS band (10 or 20 Mhz apart, near 1.5Ghz).

Is there some reason it's not totally ridiculous to expect GPS receivers to be engineered for that kind of noise?

If there's a law that says you can call in the police to drag people away if they don't shut up when you tell them to, it certainly is an issue of freedom of speech.

Perhaps you should judge replies by the standard of civil disagreement set by the essay itself.

The first paragraph of the essay says anyone who disagrees that copyright is a natural right "can go fuck themselves".