thoughtpolice

That's unfortunate. RunAbove was very nice and gave us one last year for Haskell.org (so we could port to PPC64le), and our instance is still running well (176 cores/48GB of RAM or so), but I can confirm I can't spin up any new instances.

That's a shame, they're excellent machines... I guess we'll have to find another sponsor soon.

I was saying that it brought no great advances with respect to side effects,

Sure it does. Well, side effects are boring. It's how you actually do the dance that matters. Here's a few:

- Haskell has a best-in-class concurrency story, with a far greater breadth and depth of techniques and libraries available in most languages (and some, like STM, are realistically impossible otherwise). These include many manners of graph, dataflow, (implicitly auto) parallel and concurrent programming.

- We have a nice blend of epoll based event loops with a multicore runtime, all compiled to native code. This means the traditional 'one thread per client model' is as efficient as any epoll/event loop solution. In practice, it is so cheap because Haskell threads are so cheap that it completely changes how you use concurrency, as it is almost free. It is cheap and easy to add, and the aforementioned toolbox makes it easy to do things - e.g. the `MVar` acts as a one-place blocking queue, which you can use as a lock or shared data structure, as you see fit, between threads.

- Haskell's type system has many features most other 'side effectful languages' don't offer, and even ones that are completely impossible even in things like dynamic languages.

For example, it's possible to use the type system to do things like ensure file handles are tracked statically so they cannot escape a certain scope (a form of 'region management', tracked at compile time). This is actually not even that difficult, honestly.

- Similarly, things like type classes offer a powerful set of abstractions for working with 'effectful code', and allows us to do things like easily separate interfaces from implementation. I can specify a 'Redis' type class and then a concrete implementation of this 'Redis' class, which may or may not be a fake or real. Then I can write functions parameterized only over this type class, and it works with both, and I choose which to use. If I push this further with more classes, individual functions may have a 'Redis' context and a 'MySQL' context to do multiple things; or it may only have a 'Redis' context, and no MySQL. This can be used to enforce separation.

- Lots of use of the type system to enforce all kinds of special cases and invariants. For example, it is entirely possible to use the type system to avoid things like SQL or XSS injection attacks, as done in Yesod. For the extreme version of this, the Ur/Web language takes it to the ultimate conclusion.

- Similarly, it's very easy to encode business logic in Haskell types. You can ensure things like you never mix up a "CustomerID" value with a "ClientID" value, which are really both Ints, but you can make the compiler yell when you mix them up or get something wrong.

- Haskell is a lazy language, meaning it is very easy to refactor, even I/O code. That is because you can pull any piece of code out into a name. Consider this program:

      if thing then error "bad things" else 10*2

      let x = error "bad things" if thing then x else 10*2

      h <- openThing "foo"
      doStuff h
      ... some more stuff ...
      undoStuff h
      closeThing h

   I can change this to:

      let begin f =
        h <- openThing f
        doStuff h
      let end h =
        undoStuff h
        closeThing h

      h <- begin "foo"
      ... some more stuff ...
      end h

      let withThing x f = 
        h <- openThing f
        doStuff h
        f
        undoStuff h
        closeThing h

      let stuff = ... do some stuff ...

      withThing "foo" stuff

It's actually pretty rare for businesses to write highly complex mostly functional code (a spam filter is one exception), and that is where Haskell really shines.

The term 'mostly functional code' is meaningless, because we have not even defined what it means, so it's not really useful for me to try and convince you of anything :)

Again, you do realize the 'spam filter' that Facebook produced isn't just some weekend Bayesian spam filter, right? Actual software at the scale is quite complex. I'd assume it handles at minimum tens to hundreds of millions of requests a day and integrates with millions of lines of internal code. I'm probably lowballing that, even. It's a serious piece of software.

I've tried it and I've seen its advantages and I'm content to remain with python for the time being. Python's type system isn't as good and that does sometimes cause bugs I wouldn't get in Haskell which I fully understand, but I'd consider the difference incremental. It's not any kind of great leap forward and I think my code would only be slightly less buggy in equivalent Haskell.

That's fine. But based on what I've seen (to be completely honest, not as an insult, you do not give the impression of someone who has spent extensive time with it[1]), I'd say you're greatly underestimating exactly what it is capable of, as well as precisely what capabilities it offers in the first place.

[1] The fact it should take you so long to understand it is a problem in its own way, and we should certainly keep seeking to narrow the gap between "regular ordinary programmer person" and "someone with a weird disposition for Haskell"-slash-"Someone who has way too much time"-slash-"Someone who is super persistent". Totally a problem.

On the other hand, Python has a wealth of packages and an ecosystem that Haskell simply doesn't even come close to matching.

This is certainly a real complaint for a lot of domains. It's one of the many things I could complain about. In other domains, Haskell is excellent and has quite a lot of good options. It seems to be particularly popular for web developers these days. It's definitely still pretty terrible if you want like, QT bindings on Windows.

Haskell does not eliminate side effects. It allows you to control them.

You do realize that system you described - Facebook's Sigma - is a real-time, massively concurrent online spam-fighting system, that automatically and implicitly makes your code concurrent for all operations, can optimize it, and has automated caching/batching request mechanisms in place to talk to external systems (Graph databases, SQL, cache servers) in an optimal way while reducing things like round tripping, with naive code? (e.g. it can automagically parallelize and optimize the "N+1 Query Problem" into an efficient query that minimizes duplicated requests and round trips, with no intervention, and the single 'query' can operate over multiple data sources like mentioned previously.) In other words: it does side effects all the time, and makes them manageable in ways you could only dream of in other languages. Did I mention all of that was done in a library? :)

I mean, we definitely have a sales problem, don't get me wrong. We could spit these stories better or clean up the presentation. I can list off a dozen things Haskell is poor at, or probably an infinite number given the time. But you sort of chose literally the worst example in the world to make your point.

I would suggest you actually spend some time with the language in anger. It is not easy. But I've been writing 'real world' software in Haskell for years, and it's no more difficult or 'magical' than any other part of being a software developer. It's just more rewarding because my code works far more often. And working code seems to be something that's rare in the software world these days ;)

Two very clear problems are that it introduces more complexity up front for beginners (because now to understand `length` you need to understand the concept of type classes) and the change had the possibility to break some extant code, due to it changing some type inference properties.

In practice, I think #2 was a fairly uncommon case, and the fixes were trivial and backwards compatible, so the cost was deemed pretty acceptable. #1 is a point of debate, because 'beginner' needs context (perhaps experienced programmers that are Haskell beginners would get over it quickly, but non-programmers would be substantially more confused, etc). Unfortunately I don't think we have a lot of truly empirical evidence on #1.

Overall, pretty layman slide deck (for DJB anyway) and some good notes. Was just talking about RC4/BEAST with someone yesterday.

Related slides from Peter Schwabe, documenting the `gfverify` component djb mentioned near the end, to verify Curve25519: http://ecc2015.math.u-bordeaux1.fr/documents/schwabe.pdf

Another interesting paper just from there for performance minded people, "Sandy2x: The Fastest Curve25519 Implementation Ever" - http://csrc.nist.gov/groups/ST/ecc-workshop-2015/presentatio...

IIRC, Signal/RedPhone takes a (truncated) SHA-512 hash of your phone number/email after verification of your account and sends that to the server, and does the same for your contacts. If there are matching keys, it does the exchange for you quickly and easily, and this is basically all the server does for 'user management' I think. So your friend can have their phone/email intercepted, but the central server isn't going to reveal much data or anything at least.

Second, you can verify fingerprints manually if you're in person. The biggest draw is there is no distinction between a user who you've simply exchanged keys with vs a user who's fingerprint you've verified. This is something the Threema messenger gets right. Trying to explain capabilities of the attacker and how you could be MITM'd to some random user is totally pointless and will just scare them, it's detrimental to adoption. It's far better to have a visual indication of how much relative 'trust' you have with your individual contacts, rather than write a novel implying there could be G-Men on the other side of the line.

Finally, for phone calling capability, the loop can be 'closed' through a second level of verification, because RedPhone/Signal give you a (matching) set of random words upon connection establishment, and each party says the secure words to each other before anything else. This was an idea taken from SilentCircle, I believe.

The idea here is that it is easy for a human to verify they're talking to someone they know simply if they hear their voice verify the words they're seeing, while it's probably going to be difficult for an attacker to imitate arbitrary voices on demand in real time to 'spoof' a human.

Nix is what Guix is based on. You can think of Guix as the 'GNU Version' of Nix/NixOS, meaning it provides free software packages, and IIRC it uses Guile Scheme, rather than Nix, to describe all the packages and OS configuration.

It's a toss up as to whatever you like. I think Nix has a bigger community, more packages, etc. But Guix, strictly speaking I think, is a 'superset' because changes from Nix often flow into Guix (and Guix can use Nix packages directly), as Guix is built directly on the same source-code as Nix - but not the other way around. There are some other differences, like the fact Guix uses GNU dmd while NixOS uses systemd, etc etc.

It's all just personal preference I think. I use NixOS because it's reliable and has a decently sized community, and a lot of packages. It also has really, really good Haskell support, and being a Haskell developer, that's a pretty big plus to me. Having non-free packages isn't so much of a stickler for me. I think the Guix people are doing good work, though, and a distribution for free software and the GNU project is very important - so I wish them the best even if I'm farther away.

You'd have to try both of them and make a decision for yourself IMO. But I warn you: the rabbit hole is deep, and will require learning. And when you come out - you may be immensely displeased with the current state of affairs. :)

(Full disclosure: IAMA NixOS developer.)

The point isn't the LOC. If you've never even touched C, you're not just going to have to learn that, you're going to have to learn how to write an optimizing compiler (because frankly if you've never touched C I'm skeptical you have any experience in this). And not just that: you're going to have to learn how to write the world's most optimizing trace-based JIT compiler for a dynamic programming language.

Mike spent 10 years designing LuaJIT and it is in a league of its own, not paralleled by anything else. Do not expect this inane project of yours to be solved by looking at 25,000 lines of C code. Especially if, point of fact, you do not even know C. Expect it to be 'solved' after a decade of research and hard work at minimum.

I'm not sure what paranoid reality you live in where you think this is feasible, or even desireable given your original post (frankly even though a port isn't needed Rust would be an awful choice for a 'port' due to the fact it's simply not got as good availability, the compilers and tools are less mature), but when I said see you in 15 years, it wasn't a joke - it was a conservative estimate.

Well, when the previous announcement was made, I immediately Amazon'd some C books, which I plan to devour in my free time. At which point I'll be learning Rust, and reimplementing LuaJIT in Rust, and hopefully convince Mozilla to host the git, such that it will be protected from FOSS corruption.

See you in 15 years.

I think the horsepower on those machines shouldn't be underestimated, because they are not entirely as equivalent as you think... I was thoroughly surprised when an unoptimized (but correct!) ChaCha20/8 implementation I wrote on a 3.0GHz POWER8 little-endian machine was about as fast as the latest 3.5gHz Xeons @ AES-256 with AESNI (about 1.3cpb vs 1.0cpb IIRC, but the latter has a dedicated hardware unit for it!) On that same Xeon, the ChaCha20 code only hit somewhere around 5cpb - that's software vs silicon!

It also has 170 cores and was actually a QEMU instance (w/ hardware virtualization extensions) vs raw dedicated metal. If you're doing any kind of numerical or analytic workloads (even databases), I wouldn't throw them aside so quickly. You can even get CUDA for them these days, and certain physical addons like CAPI allow you to map and coherently share physical CPU address space with FPGAs or GPUs. If I could get those things in a reasonable workstation configuration, I'd probably go for it tbh.

(I'd be more than willing to repeat this and post some more accurate numbers if anyone cares. I also need to get around to benchmarking AESNI vs that POWER8 machines _actual_ dedicated AES unit. The benchmark above was only flexing its vector/integer unit capabilities. ;)

One thing that makes it 'worse than nothing' is that it contributes to amplification attacks due to large response packets: http://dnscurve.org/amplification.html

You'll probably be fine either way, IMO - OCaml has a lot going for it, it's fast and incredibly quick to compile, and has a pretty straightforward execution model. Haskell is not quite the same (different evaluation strategy, different ways of organizing your programs), so there's a bit of associated overhead there, and for a beginner it can appear daunting.

The most important part of these languages is really how they try to enhance your abilities to write modular programs. You might be surprised to find out languages from the 1970s and 1980s have better abstractions (e.g. functors/modules) than some designed today. :)

But fundamentally I think some of it will come down to personal choice and aesthetics at some level; e.g. I really like Haskell's syntax (principled, block structured with no semicolons) and I really like laziness in general, because it makes it really easy to 'float out' and refactor code. OCaml has a much better module system, a very fast compiler, and is very well designed and thought out IMO. None of those are dealbreakers - it's just a matter of picking your poison.

We already have a cloud-orchestration solution, built on NixOS, and in a lot of ways it's already considerably nicer than some alternatives: http://nixos.org/nixops/

Docker doesn't really offer us much beyond a stable engine for actually using containers, which could probably be accomplished with its `libcontainer` anyway.

Docker's imperative scripting language to build systems isn't appropriate for NixOS, because we declare our entire system with a single configuration file, which can be transactionally updated/rolled back. That means you never want to really run 'apt-get install ...', you want to add a package to your system by modifying your configuration file, and 'rebuilding' your system. So the imperative 'run commands to update OS' model that something like Ansible uses is obsoleted.

Because of this, if I have my laptop with a configuration file, and a backup of my data, I can basically reproduce my laptop on a brand new machine on the spot by A) copying config, B) 'realizing' the configuration and rebuilding my OS based on it, C) restore data. Naturally, you normally just version control all these files, because your configuration is your specification of how to 'create a system from scratch'. All I do is 'git clone' onto a new device, run 'nixos-rebuild' and my system is ready to go. I can deploy a live server after making sure the configuration is reboot/clean-start safe by testing it in a VM, and scp'ing it to a new server, etc.

Note that the same language, Nix, is used to A) describe how to build packages in a reproducible way, B) used to describe your OS configuration (NixOS), and C) is used to describe whole configuration networks, including things like EC2 configs (NixOps). Nix is also a programming language, not like YAML or a simple configuration language - so you also get a significant amount of reuse in code, and a drop in tool diversity/complexity from this. My NixOS configurations are very abstracted and reusable for multiple situations, they share configs where it makes sense, etc.

NixOS, at least, also has a concept of Linux containers that are specified declaratively in the same configuration file. This is why I mentioned libcontainer earlier - currently, NixOS spawns NixOS-based containers using systemd-nspawn. In theory we could probably replace this with Docker, but it's not really a detail that the user is aware of - the actual underlying mechanics of the container engine are abstracted. Docker is useful as a development tool even on NixOS, but it's not really what we need. We could maybe write something more sane by reusing some code from elsewhere.

Of course not everything is perfect. Docker has of course progressed very quickly for users since I last used it (very early releases that were promising but ultimately lacking in a lot of ways), but since using NixOS I have never looked back, because while it's a tool that requires me to do a lot of work (which is not an exaggeration), it is one that actually allows me to move mountains, so to speak, and get my work done.

Sigma is quite advanced; it's essentially an online DSL where authors can push anti-spam rules (written in Haskell) into live production by reloading code at runtime. Queries are done against Sigma in real time by other services, and in turn, Sigma has to query a lot of other data sources continuously in order to determine whether a rule may fire.

For example, a particular rule about the nature of some of your friends on Facebook may need to query 10 different data sources (different DBs, caches, monitor infrastructure). One of the really nice things about Sigma is that it's built on Haxl, a library for efficient concurrent data access. It can also optimize the typical 'N+1 Query problem' away.

What this means is you can write a program like:

  ids := getAllUserIds  -- fetch from source 1 time
  foreach id as ids {
    x <- getUserFriends id -- N queries, 1 for each id
    ...
  }

There's a very good paper by Simon, the author of this blog post, discussing the design of Haxl and its use: http://community.haskell.org/~simonmar/papers/haxl-icfp14.pd... Quite the neat system!

Note: I do not work at Facebook, but I do chat with Simon a bit - this is basically the very high level 20,000 foot view from what I've read from Simon writing on the subject.

Surely, it'll never run!

Oh, the hilarious irony of giving language-lawyery, glib responses of "obviously, the code will not run" to users (who probably, you know, wrote code with the intention of it running) - users who are complaining about language lawyering optimizing compilers in the first place. It's like two people reading the same page in a different book or something.

Are you being serious, or just trying to sound super philosophical about why "less is more"? I assume it's the latter, because it shouldn't take very much thought to see why HTTP servers are fairly complex pieces of software, given the purpose they serve - a class of software that is ruthlessly optimized in today's world - nor should it take very much thought to see this HTTP server is actually ridiculously inefficient compared to any modern one. You know, wasting all those precious CPU cycles you opine so much about?

(Now, if you want to talk about the actual efficacy of HTTP vs other stateless protocols, that's a different story... But I doubt we're going to go there in a thread about an assembly HTTP server where people are ooh'ing over the achivement. Not that it isn't cool, TBQF.)

Programmers at large really need to stop being pretend philosophers clutching at straws about "why things are so darn bad today!!!" (among other psuedo philosophical positions). They're mostly terrible at it, and it's almost always just so damn hamfisted and full of itself.

https://www.metabunk.org/dr-kirkby-2009-cern-presentation.t5... whoa man, it's almost like you can use google! BTW, Harold Saive is a well known chemtrail conspiracy theorist who has outright lied on several occasions before. He surely doesn't have anything to gain from misrepresenting a scientists results, does he? https://www.metabunk.org/outrageously-fake-chemtrails-video....

As for the Harvard results, the results aren't as important - it was meant as the joke that "The government is doing it to control us". You know - the conspiracy theory, just like all the other ones, which if you wanted to counter my claim (which wasn't even the point for fucks sake), you would need evidence of. As opposed to some chemicals having unintended side effects, which is possible (and happens).

I like how you also conveniently ignored the rest of my post, and didn't actually explain your point about inflation. Instead, you just said "well, it's obvious bro". How explanatory!

I'll take that as an indication you don't know what you're talking about. Thanks for playing!

You didn't answer his question as to where this 'clear mass disillusionment' is. Where is the actual proof fiat is on the way out?

Hacker News: where some people legitimately believe that the entire world will abandon the current credit/monetary system, because reasons (or alternatively, "just because" - you know, to see 'how it works', because an entirely new monetary system is like testing on some FiveFinger shoes to be spontaneous).

Also, Bitcoin is totally an invention by the Fed to ween people off fiat, despite the fact the Bitcoin network and its total overall volume are a joke compared to global currency trade, and basically worse, or completely irrelevant, for consumers in pretty much all cases.

If there was any ever proof techno libertarian supernerds are insanely disconnected from reality, stuff like this is it. You have a better chance of actually being The Highlander. But seriously, I could write a comedy novel about this stuff at this point - so do continue to go on.

If they can't abide by the rules that the state have set for them - in this case, what seems to be a fairly reasonable a ruling saying that their 'contractors' are actually employees - and they can't make profit with those changes, then their company should die, or reform. That's basically all it comes down to. If their company is downsized as a result, well, you can blame them for unsustainable business that didn't actually work when the alarm finally rang, and their inability to respond.

If your friends want a startup that will help them get downtown to pound beers faster, and Uber dies, don't worry - someone else who can _actually do the job_ and abide by the rules will almost certainly be there. And the Uber employees who get canned? They might actually

The amount of doublethink people have here about "bad actors will get pushed out of the market for better ones" while simultaneously defending shitty business practices, or conveniently ignoring that bad actor principle when their oh-so-favorite business gets a slap, is pretty astonishing. But given most people on HN seem to only want to "disrupt" the wallets of other so theirs can get fatter through acquihire buy-out plans for their ephemeral startups, I guess it's not surprising.

It's worth clarifying this a bit because there are a lot of subtle implications about what it means to be 'reproducible' or 'deterministic'.

To make the terminology clearer, I like to use the term 'deterministic' vs 'reproducible'. A deterministic build is one which, if it works, will always work, and follow the same steps. A reproducible build is one that you can reproduce identically, down to each individual SHA1-hash. This is what Debian has spearheaded, and what they mean by 'reproducible build'.

At the moment, Nix packages are deterministic - but they are not reproducible.

If I have a specific git revision of nixpkgs (the repository containing all package descriptions), and I say 'install mutt', I'm guaranteed that I will always get the same build results. No matter when/where I do it. That means I'm always going to get mutt version x.y, with dependencies A, B, and C, all with their own exact versions, and features enabled. The same optimization levels. The steps the compiler uses to build everything will be the same, etc.

You can essentially think of a 'nix expression' as a program that gets compiled to a shell script, which does a build, and you run the shell script. So if you have git revision DEADBEEF of the 'nixpkgs' set, and you 'run the compiler', so to speak, to generate a 'builder' from a Nix expression - it seems very obvious it will do the exact same thing, every time, regardless if you run it today or next week.

The thing is, this is a pretty nice property. In Debian for example, if I 'apt-get install' something, I may not get the same program if I do it today and then do it tomorrow, because it may get updated. This, in practice, is kind of a big deal actually. It means it's impossible (unless you use your own mirror) to actually have things like prod/development environments the exact same without imaging them like Docker. And of course, this makes rollbacks impossible because the set of packages on your system is really a bunch of mutable variables.

For example I used to do security research, and it was a massive pain in the ass when I would try to 'apt-get install' mysql and get a patched version already. I needed to write code to find this vulnerability, AND I want to regression test that code in the future. But I can't. It makes it very hard to do things like write automation to make sure you can detect if mysql is vulnerable (because where will you get the pristine package you originally tested with?)

Similarly, because of this property, you can be sure a developer's computer is exactly the same as a production or staging environment for example. Because the 'state' of your whole computer is really a function of two arguments - a function of your configuration.nix and your nixpkgs package set. This is what it means to be a 'purely functional' distribution!

But the builds aren't reproducible yet. There's all kinds of actual 'non-determinism' in the build process for any one specific project that makes bit-for-bit reproductions difficult. For example people use `__DATE__`, or they do weird things like rely on build mtimes, or other crazy stuff. Debian has tracked tons of these down - so it's doable!

There is a branch of Nixpkgs that aims to fix this. Hopefully it will be solved for NixOS 15.10.

The runtime is SMP-capable and lightweight threads are preemptable, multiplexed on top of epoll (or kqueue) based event loops. So it's a preemptive N:M model. Haskell threads basically try to behave like OS threads as much as possible (with semantics that look like they're blocking) but they have a lot better cost model overall, so you don't need to do manual callback-based programming. It's pretty nice.

There are really dozens of concurrency abstractions you can choose from, and yes, CSP-style programming is an option, available as a library: http://hackage.haskell.org/package/chp - and common abstractions like MVars (which are essentially simple, concurrent 1-place queues) can get you a long way even without that.

There are other libraries for more specific needs; like graph/dataflow based parallelism, array parallelism, GPU-based programming, DSLs for image processing, etc etc.

All that said I'm very happy and hopeful to see OCaml 4.03 adopt multicore support. OCaml has an excellent, robust and lightweight toolchain and implementation, and is very straight-forward and powerful out of the box. It's not my personal cup of tea, but we'd be worse off if they weren't here.

As far as I know, that's never really been a reason as to why we haven't implemented it in GHC. It's much more likely just that nobody has ever gotten around to implementing it. Shouldn't be especially hard, I imagine.

There is Upcast[1], which is a different tool by Zalora and does this - it simply adds a file you can check into the repository for developers to use. It has some beta-ish limitations but the idea is what you described, basically.

The remaining build step, then, is copying the new closure of the environment to the machine on deploy, which can take some time depending on your network. Instead I think what you'd probably do is use Hydra (a CI server) to actually build the packages/closure of your network on every commit to your repository, and then add that server to your actual deployment server's binary caches - that way when you deploy things after CI allows it, the needed assets will already be on the remote (faster) binary cache, within your network.

[1] https://github.com/zalora/upcast

Hm? The graph on the page shows 4.5% of contacts being marked as "Unable to contact", while it shows a very small 0.5% as "Refused, Code Rewritten". Or is this graph wrong?

I also highly recommend Phabricator - it has excellent tools, active (paid) developers who are excellent people, and is very easy to maintain and use. I also think it simply scales to bigger projects much more effectively than GitHub (in some important ways - like emphasizing rebase and small, continuous development, a better UI, and better notification and commenting/review system as well). That's just me, though.

We use it for GHC, and I've had bugs fixed within 10 minutes of finding them on our live install thanks to the devs. They've also helped us write extensions and customize our Phab install. We've had a very good experience all around.

Well, it's saying more than that. It states that the notions of 'equivalence' and 'isomorphism' are basically the same thing in this new language (NB: I'm not really a mathematician).

Equality is already a very overloaded term in mathematics, but roughly means "these are the same thing" - X^2 is 'equal to' X * X for example, or in most cases we think simply of the identity relation on some set or whatever. Isomorphism states that two things can be 'transformed' into each other through the existence of a function, along with its inverse.

For example, the sets {A, B, C} and {1, 2, 3} are not equal, but isomorphic because you can define a bijection between them: A = 1, B = 2, C = 3. In some sense equality is 'more rigid' than an isomorphism, obviously. Also, you have to choose the bijection explicitly here because in this case, more than 1 valid one exists, which is another aspect of an isomorphisms 'identity'.

The univalence axiom states that in this new constructive mathematical framework, 'equality' and 'isomorphism' are exactly the same thing.

I suppose in some sense you can view concepts like "object identity" and "object state" in some languages like Java in the same bucket, because while two Java objects may be "equal in terms of state" (members all the same) they might not be "equal in terms of identity" (because they point to different heap objects).

But this kind of distinction mostly doesn't make sense in functional programming languages because you often throw the notion of 'value identity' out the window, so 'equality' in these languages is defined solely as mathematical equality - that we can 'normalize' two expressions to the same final form. 'isomorphism' then, normally just has an interpretation like two functions `a -> b` and its inverse `b -> a`, so even in these languages, we aren't quite talking about the same things.

HoTT is much more radical than all of this when you look at it together of course - because it's more like saying if you have two proofs that x = y, you can think of 'x' and 'y' as points in space, and proof of equality is a path from x to y in this space - so two proofs of equality are just two distinct paths.

The 'space' on which these points exist is actually not sets but 'types', which is like a set, but also including propositions too. So now the set 'X' and propositions about X exist together. Proving some proposition requires 'constructing' a value of that propositions' type, using the elements and propositions already existing. In a language like Haskell, to implement a function of type 'f :: A -> B' requires being able to 'construct' a B given a value of type A - to do this, in effect, is a proof that 'A -> B' does in fact exist, because you built it.

Also, under this interpretation of 'space', which is topological, equivalent paths give rise to notions of 'homotopy' (saying a path A can be 'morphed into' a path B), so if you have two 'paths' representing the proofs of x = y, these 'paths' admit a homotopy between them. And furthermore you can have notions of homotopies between homotopies, etc etc. So things get very 'higher order'. Types can also be viewed as an 'infinity groupoid', which is a thing that not only has elements and isomorphisms between elements, but isomorphisms between isomorphisms, and isomorphisms between those, infinitely. So if you squint you can see how this infinity-groupoid notion of 'higher order' isomorphisms between other isomorphisms, and higher order homotopies, are all very closely linked. It's all very strange and unifying and delightful.

That's the extremely handwavy explanation that is might be pretty fluffy, but it might help.

GCC 5.1 defaults to having color diagnostics set to `auto`, meaning it will display nice, beautiful diagnostics like Clang does on your terminal, if that's what you're referring to. (You can also get these with GCC 4.9, too, using the `GCC_COLORS` environment variable).

Personally I don't care about that as much as the optimization improvements this time arond, it seems. Better devirtualization? AutoFDO? Reuse of the PIC hard register, especially? (That will be a great win on 32 bit machines, and makes it all the more possible to enable things like PIE for 32-bit applications, where it would otherwise be a big penalty, as well as many other things.)

Power usage is very important for low-end devices, especially smartphones which will be talking to lots of HTTPS resources. This is the complaint on the other side of the pond, away from the people who need ASIC accelerators for whatever reason to keep up with bandwidth/latency/cpu concerns.

Just as an example of the difference - I wrote a naive implementation of ChaCha20 in C with zero optimization effort and it does 5cpb out of the gate (Sandy Bridge). Just using vector-types and letting GCC/Clang vectorize brings that down to ~3cpb on Sandy Bridge - no effort. The Krovetz implementation of ChaCha20 is closer to 1.2cpb on my machine, with AES-256 doing 1.0cpb using AESNI (again, my own naive implementation). All software.

Even the most hand optimized, secure AES software implementations are still in the realm of ~15-20cpb (IIRC), three-to-four times worse than the unoptimized competitor. As linked elsewhere in this thread by me, non-scientific tests show it 3x faster in software on some mobile phones. That's a lot of extra cycles-per-byte for your battery to chew through using AES-256, and I'd guess I easily churn through a low number of gigs of HTTPS data every month..

This point is important, because there is a lot more non-AESNI hardware than the converse. But luckily, it's possible (and likely, I hope) that TLS 1.3 will include the ChaCha20-Poly1305 AEAD ciphersuite, which should improve this matter quite a bit for most users who need software implementations - it's _much_ simpler to implement, and even in software, a heavily optimized can get within the ballpark of AESNI.

Google is already using ChaCha20-Poly1305 inside Chrome to talk to Google servers, if your hardware doesn't support AESNI. It's been doing this since early last year, and Adam reported at that time nearly 40% of all traffic to Google was going through it (including mobile devices IIRC): https://www.imperialviolet.org/2014/02/27/tlssymmetriccrypto...