staunton

36 ms·

571.
by staunton 3y ago
Some candidates: Scandinavian countries, Switzerland, the Netherlands, Taiwan (esp. considering the circumstances), New Zealand.
572.
by staunton 3y ago
Preprint by DJB on the use of computer-checked proofs, particularly for cryptography
573.
Papers with computer-checked proofs [pdf](cr.yp.to)
3 points by staunton 3y ago|1 comments
574.
by staunton 3y ago
I don't see how that relates to the question of "does Mathematica allow users to define simplification rules?"
575.
by staunton 3y ago
That's very different from benefit. Also I don't see how that's related to what your original comment was arguing for (cost of replacing stoves). Maybe I should add that I do agree with your conclusion (that replacing the sto
576.
by staunton 3y ago
While this is a tiny contribution to global warming, funny enough, it turns out that reducing this kind of emissions is also very cheap. To the point where you get very solid emissions reduction per dollar spent.
577.
by staunton 3y ago
Soil damage only happens where it happens while warming can significantly reduce arable land on the planet. This matters a lot for feeding people. That doesn't mean we shouldn't care about maintaining soil qualiy but your commen
578.
by staunton 3y ago
The problem is that it will be a lot harder to grow food after 3°C of warming and also to get people drinking water. At some point your "deepening relationship" has to feed billions of people. That's assuming the heating is
579.
by staunton 3y ago
This assumes that what people pay for power is determined by how much it costs to produce. That's already not the case in most countries. Energy prices are determined by taxes and subsidies.
580.
by staunton 3y ago
Maybe there is a way to be sure of that but "benefit" isn't even a concept in "simple thermodynamics". That's not an argument for anything.
581.
by staunton 3y ago
A CAS also covers only a tiny part of "an undergrad math degree" so that's beside the point here. Assuming it had appropriate tactics doing the job of a CAS using all theorems (which isn't happening any time soon), what
582.
by staunton 3y ago
Julia's Symbolics.jl allows users to easily add custom rewrite rules. However, it's not a state-of-the-art CAS. I don't have that much experience with others. Mathematica doesn't allow it, I think.
583.
by staunton 3y ago
Fair enough, that would be nice. However, it sounds like a very hard thing to build in practice. I'd expect, actually, it's best done in Lean itself. So you're proposing a CAS written in Lean, which noone is currently working
584.
by staunton 3y ago
Lean does have a tactics system (very similar to Coq). However, there is no general tactic that will do, e.g., "sin^2 + cos^2 = 1" for you. (Writing a tactic specifically for that simplification is easy, of course, but that&#x27
585.
by staunton 3y ago
That's an entirely different thing though. Good luck getting Lean to help you do any symbolic computation whatever. You can use it to prove that a given manipulation is correct. You cannot use it to find a result (there may be a
586.
by staunton 3y ago
Library developers can afford to deal with complexity much more than users of libraries. Offloading such work on highly skilled people developing the basic infrastructure is surely the right approach.
587.
by staunton 3y ago
More like "deploy once ever, maybe"
588.
by staunton 3y ago
There's some software where it's important not to have bugs and know exactly what it does, and some where any attempt to specify what it's supposed to be doing, let alone fixing all the bugs, is a waste of time. (And things i
589.
by staunton 3y ago
Maybe not the average but the power is concentrated in a few and they are also affected. I'm expecting many who collectively do have power to participate in shaping how these things are used and perhaps oppose the big companies.
590.
by staunton 3y ago
I strongly disagree that these are big problems in practice. There are macros you can use to make newtypes more ergonomic to use and reduce boilerplate, etc. The advantage it gives is forced adherence to many implicit assumptions of library
591.
by staunton 3y ago
But, contrary to at any such developments in history, the people who are losing out aren't the "poor working class". They already have cultural and political power that they stand to lose. This might still go a lot of ways.
592.
by staunton 3y ago
They aren't assumed to be bug-free. It's simply known that the vast majority of bugs that occur in practice and that you have to care about aren't compiler or hardware bugs. So formal systems have a lot less bugs.
593.
by staunton 3y ago
The way I would phrase it, the difference is in what kind of doubt is considered "reasonable".
594.
by staunton 3y ago
My comment was parody. Surely, nobody actually says things like that?
595.
by staunton 3y ago
The thing that these systems offer is "having to check less code". In some situations, that's huge. In others, it's not worth the effort it takes to get there and maybe doesn't actually reduce the complexity of chec
596.
by staunton 3y ago
So, that would be "I think you did it wrong; of course, I can't claim to know that objectively; anyway, I really liked the way you did it"...
597.
by staunton 3y ago
There's a huge gap between "cold turkey into starving" and current goals (which are still not enough and also mostly won't be achieved). A transition away from fossil fuels that was just constrained by ensuring no mass s
598.
by staunton 3y ago
> to keep planetary civilization running Did you mean: "to never decrease consumption in rich countries"?
599.
by staunton 3y ago
Most people in either region are not making any significant effort. They just live their lives like everyone else around them. The difference is in what that looks like. Anyway, what's with this dichotomy "corporations should chan
600.
by staunton 3y ago
While I agree with the prediction, the tone they use seems somewhat too close to "well, if we're not going to make it anyway, how about we sell some more fossil fuels?"

More ›