Hacker Newsnew | past | comments | ask | show | jobs | submit | mantraxC's commentslogin

Hmm, given how compilers & hardware can introduce incorrectness and security vulnerabilities in otherwise valid code, it makes you wonder if anyone can really claim "end-to-end proof of correctness" unless they include the specific compiler & hardware in their proof.


Concerning the compiler, in the link it is written:

"There is a further proof that the binary code that executes on the hardware is a correct translation of the C code. This means that the compiler does not have to be trusted, and extends the functional correctness property to the binary."

(I wonder how that works but it is related to your compiler concern)

Now even though the issue of hardware (say rogue hardware with rigged number generators and whatever backdoors) is probably a real concern, I still think that seL4 and its codebase where hundreds of bugs have been automatically found (and manually squashed) is a big step forward.


On that note: what even is a correct translation of C when it has so many undefined behaviors in it's spec.


They use a formally-specified subset of C described in Harvey Tuch's PhD thesis: http://www.ssrg.nicta.com.au/publications/papers/Tuch:phd.pd...


What if the code doesn't rely on undefined behavior?


Absence of undefined behavior in the C implementation is of course one of the things covered by the seL4 proof.


Oh, Jesus, this looks like the unfortunate result of a Windows Phone and an Android phone in a teleporter accident.

Many here are cheering as if this is good somehow, because Microsoft is open and what not. But look at it. It looks like Windows Phone, but is an Android phone. It exists to confuse customers.

What is the supposed end game here? "Hey, buy this and if you like it, we'll make you abandon all your Android apps, and switch to real Windows phone - because the home screen tiles look similar"?

I don't think so.

This project is more the result of a slow-moving corporate behemoth that started this project way before Microsoft announced it's buying Nokia. It was too late to turn that giant ship in time, I guess, so enjoy your mutant monster.

By the way, the startup sound is Ripley whispering "Kill me" in your ear.


It'll be interesting to see how they plan to market this to people, because I have to tell you... "your thermostat integrates with your car, washer and jawbone bracelet" is damn confusing to me as a value proposition.

Yeah I see the potential, but even though I'm a programmer, I see a lot of random shit put together, and no clear reason why I should go through the effort of building a mental model around it in order to understand their vision.

HomeKit is just a set of APIs right now, so we have yet to see if it has legs, but it centers around a versatile device I always have with me - my smartphone. It makes far more sense to make smartphones the hub, so focus it around Android, not the thermostat...

The Google-Nest relationship is a bit toxic right now and people are all scared that their data is going to leak the Google way. But we all know it's going to happen, why delay the inevitable with this forced, confusing vision of the home?

I've seen such integrations fail before. Apple had those weird wireless iTunes / iPod / Hi-Fi integrations in the early 2000s and it never caught on, because it was damn confusing (and plugging the speaker audio cable in your iPod was way simpler).

This stuff needs to seem simple and inevitable, so people say "but of course I want that". And this is not it. It looks complex and arbitrary and their own ads videos say "people might say, why are we doing this". If you anticipate people might say that, you've failed.


I expect they will market the dishwasher as saving a bit of money when you have the thermostat. Similar with vehicles, it's a feature to check off when you are at the dealer.


Those home automation products are marketed to the people who have the money to buy such fancy home automation widgets.

Those people also typically want to "save the environment", but I doubt they want to save it so much, that shaving a fiver off their power bill means they get a thermostat tell them when to wash their dishes and do their laundry.

Putting the dishes and clothes in and out is still a manual activity, so this makes absolutely no sense to be scheduled by a thermostat, unless you have waaaay too much free time on your hands.


Right. I'm saying that I expect the marketing to be at the point of sale of the dishwasher and to be rather mild, so that it mostly targets people that already own a compatible thermostat. Or in press releases and the like.

I think home automation is mostly composed of things that sound neat and provide modest utility; Nest might pay itself off faster, but most buildings would see more benefit from increased insulation. Something like programmable lighting is fantastic, but it probably isn't going to save much money or energy, and switches just aren't that burdensome. I'm glad there are people trying to figure it all out, at some point the cost might get low enough where "neat" is enough justification.


I think you're confusing JS minification with obfuscation. Minified code looks obfuscated, sure, but it's not done to deter "hacking", just to make the code smaller.


The code in the challenge isn't even minified, it's just really minimally obfuscated. So, no confusion here.


I'm not talking about the challenge, but those supposed commercial JS libraries with DRM that you're advising "should take notice".

There are no mainstream examples of such libraries. You're likely confusing minified libraries for having an intent to obfuscate, or talking out your ass.

One or the other.


Yeah? Go take a look at GoJS. Then sulk off to whatever fetid corner of the internet you came from.


They say that, but there's one giant missing ", because..." in that paragraph.

They never explain why they render in 10 sizes (why don't they know which sizes they need), and why is loading one of those sizes on a mobile app not feasible.

It's stated like that and left hanging in the air.

Either their use case is very weird, or they're deliberately vague for some reason only they know about.

Also to clarify why 10 sizes is weird, normally what you'd do is double the width/height of your images with every size (so quadruple the pixels), same as one does with mip-maps. Or with icons.

Let's say the smallest sensible size is 128x128 (minimum needed to discern a product, and easy to downsize from there, won't get much smaller at good quality).

So we have 128, 256, 512, 1024, 2048, that's 5 sizes. And I'm pretty sure the images they need aren't over 2048x.

So 10 sizes is just pointless.

And with OpenRoss, doing cropping and adding whitespace at the server, producing pointless image duplicates, is senseless. Even the most crippled client-side technique can do the cropping and whitespace for you (yeah, even html).

This screams "we didn't think this through much".


When the site was originally designed, there were only 4 or 5 sizes, one for the feed, one for the product page, one for related products, one for thumbnails, etc.

As the design changed, extra sizes got added to the image processing, and as with most early stage start-ups, it worked therefore there was no need to fix it.

We eventually ended up in the position of having 2.5M products all with preprocessed images of certain sizes from our design history. As we wanted more flexibility with design, but also knew that a lot of our images would have a very low likelihood of being accessed (fashion items have single runs and are never remade in future seasons), a big batch process didn't seem appropriate. Additionally, it would mean storing several different copies of images in our S3 bucket, even if we knew the product would not likely be seen again.

A more attractive solution (at least to us) was to do the hybrid approach, where we would resize on demand, and then cache for a long time. This way, we only do the processing for images that need it, in almost a functionally identical way to large scale batch processing, but the process is demand-led.


But the nice thing is - using a storage solution where you don't pay for what you don't use.


It's a chicken/egg scenario. How does the resource cost of resizing on-demand compare to storing all sizes? Also, like @mantraxC said, are all those image sizes really needed?

I have a system I'm trying to sunset that has a 160 and 130 size. Totally redundant, and doesn't really save that much space/bandwidth.

Still, OpenRoss is a cool project to learn from. It might not fit many use-cases, but apparently it works for Lyst.


I have had this exact problem/need overtime on several projects, and it doesn't mean "we didn't think this through much". Products change/grow and there becomes a need for tens of different images. First it starts with a thumbnail or two, then composite images, then, etc. Not to mention you need 2x images for retina devices.

Bottom line, overtime you tend to understand that there is great flexibility in this type of architecture.


"This screams "we didn't think this through much"."

That's actually quite rude.


"Even the most crippled client-side technique can do the cropping and whitespace for you (yeah, even html)."

Facebook, Twitter and Google Plus all have a feature where a URL gets expanded out to a "rich preview" (Twitter Product Cards for example are particularly relevant to a site like Lyst: https://dev.twitter.com/docs/cards/types/product-card )

These all work best with an image that has been pre-cropped and resized.

As an added bonus, a new one of these emerges every now and then - with a different size requirement.


At scale, processing thousands of highly granular items (images) in any way is an embarrassingly parallel task even in its most crude and naive implementation.

So claiming "fast", ok, but claiming "scalable" feels like a redundant buzzword, a bit hand-wavey.

When you make such generic claims, be quick to explain what you mean, or people will not treat you seriously.


Yeah what i was thinking. There is no state to be managed. Its just a pipeline which doesnt not anything more than more machines to handles more load. Its relatively easy to implement.


So how many people's lives were saved by this coverage and condemnation, that's the real question.

I don't think some country's ruler gives a damn about coverage and condemnation, as long as it stops there.


With respect I disagree. The most metallic of tinpot despots still believes themselves to be righteous and want to be loved and admired. Amnesty International's experience is that such rulers care sufficiently when a bunch of ordinary people write them letters for that to be a worthwhile thing to do in support of political prisoners. Worthwhile along useful dimensions like stopping torture and so on.


Who needs prank calls when we can troll the comments sections of news websites.

Wubba lubba dub dub!

Plus... honestly: "underappreciated prank calls". You gonna talk about some ancient childish nuisance behavior as if it's a red book animal species worth protecting?

Jesus, nostalgia is a powerful reality distortion field. Next thing, people might start talking about how scratched dusty vinyl records sound better than lossless digital audio.


I posted this because I found it of particular interest that the blackmailers ask for payment in Bitcoin.

It makes you think if Bitcoin is turning into a giant example of "be careful what you wish for".

We have exchange after exchange get hacked and legit Bitcoin users losing their money, and now Bitcoin enables extortion schemes that couldn't work so effortlessly before.

Where is this going?


Bitcoin is only pseudoanonymous. At some point, the 'bad actor' has to access 'legitimate' banking institutions to exchange the Bitcoins to fiat and that is the weakest link. It requires reporting to relevant tax or other authorities based on arbitrary (and secret) amounts, but targets money laundering, drug trade, gamlbing, etc.

I suppose if I had to throw a potentially disruptive idea out there, you could create a database of 'blacklisted addresses.' Let's say when Bitlocker came out, you entered that address into a database and it was verified as being associated with this scam, well it is trivial to track those coins between addresses and every address it enters is blacklisted until it enters a mixer or exchange, at which point you have a potentially complicit corporation that you could actually target with the subpoena or other legal action for discovery of IPs, login, etc.


People have suggested this before. A bad actor then just takes 100 illicit bitcoins and sprinkles them in random amounts across many addresses, 11 to himself at another address, 6 to a non-profit, and 14 to you. You are now indistinguishable from the bad guy.


I can't say I would complain if thousands of dollars was given to my address, but you are right... it would represent a difficult problem for enforcement and creative people would come up with clever workarounds.


> "At some point, the 'bad actor' has to access 'legitimate' banking institutions to exchange the Bitcoins to fiat and that is the weakest link."

And on the contrary they can do the exchange in, say, Nigeria. So Bitcoin's weakest link is also the law enforcement weakest link, because no one has authority over the entire world, and there are plenty of spots where you can do the exchange without trace.


> Where is this going?

Not far's my guess. If BTC gets too popular as a tool for extortion and money laundering, then the authorities in developed countries are going to start carefully monitoring people who sell large quantities of BTC for sovereign currency or commodities. It would just be another part of their general efforts to combat organized crime. That would make major speculators feel less welcome. If major speculators decide to take their ball and go play somewhere else, the price of BTC will probably tank. That'll discourage everyone else. At which point BTC becomes a terrible medium for money laundering because nobody wants to buy them. I also suspect that the relative anonymity of any one transaction is closely related to overall transaction volume in the BTC economy.


These organizations aren't in developed countries, so their potential cash-outs wouldn't be noticed. Going forward, I would expect even more of the expenses of running an online criminal operation to be payable in BTC, so you wouldn't even need to convert it.


Bitcoin — assuming it works — also becomes the perfect currency for kidnappers and blackmailers. Awesome, huh?


You mean like straight cash has been up until now?


Yup. Except straight cash still needs someone to physically collect it which leaves a point of failure in the crime and a good place for authorities to catch the bad guys. Bitcoin removes that.


But gives another ways to track the money that was paid. It's a matter of authorities catching up with the technology.


The very nature of it makes it much easier for criminals to avoid authorities once payment is made though. Sure you can screw up and do something stupid like send it to coinbase and cash out but there are lots of ways to use it without the authorities being able to determine your identity or location.


yup, we can't have the cake and eat it too. we have to learn how to minimize risks and keeping bitcoin alive


Nice, we're evolving the same mechanisms for quick herd notification that animals have.

This is why humans and animals scream when we're in danger (not because screaming is a very effective danger mitigator), and this is why some animals jump in place when they detect danger (http://en.wikipedia.org/wiki/Stotting).

We've had these two signals exploiting our vision medium, and our sound medium. And now increasingly, we're adding signals exploiting our digital network medium.

As those become more and more commonplace they have a very tangible effect on our society. Think Twitter riots and what not.

BTW, people in Japan get an instant smartphone warning when there's an earthquake.


> BTW, people in Japan get an instant smartphone warning when there's an earthquake.

To be specific, BEFORE there's an earthquake. Otherwise it wouldn't be very useful :) And it's not just smartphones, this system is in place on dumbphones well (using the GSM Cell Broadcast feature).

Americans get an instant smartphone warning when a child has been kidnapped http://www.imore.com/amber-alerts-your-iphone-what-they-are-...


> To be specific, BEFORE there's an earthquake. Otherwise it wouldn't be very useful :)

To be even more specific, after the earthquake has been detected, but hopefully before the seismic waves reach their location. Otherwise it would be magic ;)


> To be specific, BEFORE there's an earthquake.

Yes, it takes a little while for seismic waves to travel from the epicentre to locations a fair distance away. The high speed trains are programmed to start braking as soon as an alert is heard - it's usually enough to shed 100mph or so off the speed before getting in trouble.


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: