skew · HackerTrans

skew

no profile record

comments

5년 전discuss

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.

8년 전discuss

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

9년 전discuss

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)

10년 전discuss

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

10년 전discuss

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).

11년 전discuss

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!

11년 전discuss

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.

11년 전discuss

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.

11년 전discuss

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

12년 전discuss

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".

12년 전discuss

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.

12년 전discuss

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.

12년 전discuss

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.

13년 전discuss

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

13년 전discuss

"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.

14년 전discuss

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.

14년 전discuss

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.

14년 전discuss

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?

14년 전discuss

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.

14년 전discuss

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

Iterators do nothing for parallelism either.