danparsonson

You give the answers to this in the artcle:

> The most substantial finding was a heap buffer overflow! but, not in lean-zip's code, but in the Lean runtime itself. (emphasis mine)

> The OOM denial-of-service is straightforward: the archive parser was never verified. (me again)

"Lean proved this program correct" vs "I found bugs in the parts that Lean didn't prove was correct". The failure was not in Lean's proof (which as I said is heavily implied by the title), but in ancillary or unverified code.

Do I misunderstand how Lean works? I am by no means an expert (or even an amateur) on Lean or formal systems in general. Surely the first class of bug could be found in any code that uses the framework, and the second class of bug could happen to any system that isn't proven? Does that make sense? Otherwise where's the boundary? If you find a bug in the OS, does that mean Lean failed somehow? How about the hardware? If your definition of a 'formally verified system' goes beyond the code being verified and the most important thing is whether or not you can make it crash, then the OS and the hardware are also part of the system.

Of course bugs are important to users regardless of the cause, but the audience for your article seems to be software engineers and as a software engineer, your article was interesting and you found something useful, but the title was misleading; that's all I'm saying.

We're not speaking about bugs in a verified system so much as writing articles making specific claims about that. Surely if we're at the level of precision of formal verification, it's incumbent upon us to be precise about the nature of a problem with it, no? "Lean proved this program correct and then I found a bug" heavily implies a flaw in the proof, not a flaw in the runtime (which to my mind would also be a compelling statement, for the reasons you describe).

Sure - what I mean is that being able to run an equivalent GUI to Windows (Gnome, KDE) using less memory than Windows requires is a benefit, but not the most important one to me. There are other bigger benefits to using Linux+GUI instead of Windows than saving on a bit of RAM.

Or, you know, rest :-)

Other costs? Deviations in the actual figures from the estimates we're using here? 100 is not a million miles away from 129.

As long as you use the best parameters then it doesn't matter

Not to mention that 'lower memory usage' is only one of many benefits and, at least before the prices went mad, hardly the most important one on the list.

What's wrong with whales?

Did you spend your entire life in isolation from the rest of human society? Because if not, then you have been influenced throughout your life in a multitude of subtle and not-so-subtle ways by the works of others. In what way, then, are the fruits of your head entirely yours? We're all standing on the shoulders of giants.

So are we arguing that the article that talks about them using ASICs is just making that up then? Otherwise what's the fourth option?

Who says CERN needs to be cost effective?

Could they.... have someone else do it for them?

On the other hand, if you punch someone in the nose and then loudly declare that your treehouse is the only safe place and everyone else is forbidden from entering because people have been punching people in the nose lately, then that does have a ring of hypocrisy about it doesn't it? The US is not banning its own routers.

For one thing, sandboxing does not prevent apps from using IPC to talk to each other, so Google Play can communicate and thus share data with other apps regardless of the user's settings.

Wine is not a full reimplementation of Windows, so not an analogous situation.

What kind of attack are you anticipating? Surely only a fool or a madman would make such a thing publicly accessible.

Doesn't 'a job I hate for not enough money' describe like 50% or more of the world's workforce?

True although prices are also not what you'd consider average in a developed country. Purchasing power parity is important too.

You're joking, right? Haven't you heard the stories of people having 'relationships' with their chatbots? Far from getting bored of these things, we're getting hooked on them.

Wonderful! What a cool idea. For anyone interested, you can learn the whole of Hangul in an afternoon; it's cleverly designed to be very logical and has some handy mnemonics: https://korean.stackexchange.com/a/213

You can't just spin up such a facility in a few days or weeks though, surely? Even if the core of a process is relatively simple physically, you still need all the supporting infrastructure to make it happen.

> ...I wonder how much kinetic energy it had...

Since kinetic energy is proportional to v squared, that highly depends on how you measure v...

You can override the matching method on an individual basis though, just using the setting button next to the URL entry field.

I don't think your original post suffered for the lack of one more TLA acronym.

No, a lawyers opinion will reflect the law. From a legal standpoint it doesn't matter how you feel about applying a license to your work, it matters what the law says about that. I'm not a lawyer, but my expectation is that the license you choose will bind anyone who chooses to use your software, and in particular will have an effect on companies that wish to use it. That may be fine and exactly what you want, but my point is just that it's not necessarily a whimsical 'statement of intent'.

It would be interesting to hear a lawyer's take on that, as I suspect their opinion might differ from yours...

Yeah that describes most legacy codebases I've worked on XD

> ...the challenge with writing tests well...

Sure, you can test more or less anything given sufficient time and force, but a massive fragile harness wrapped around the system under test is not what I mean by 'testing well'.

Also there are other things in software besides web; unit testing code that is entangled with desktop UI can be difficult or impossible without changing the original code. Try testing a WPF app that talks directly to the Dispatcher when there is no UI thread, for example.

What's the difference when booting off a USB drive? That's been my goto in the past when I forgot my login password; does the TPM only unlock boot devices?

And the challenge with writing tests well is that it might be difficult or impossible without the refactor...