staunton

28 ms·

451.
by staunton 3y ago
> everyone will apparently just shut down and not do anything about it because why bother A negligible (both in terms of numbers and wealth) part of the world population feel this way. I guess most people actually still barely think abou
452.
by staunton 3y ago
It's not useful to prove that "your program does what you want, provided the following 10000 functions implemented in C do what we assumed they do". Almost certainly at least one of them doesn't. There isn't even a
453.
by staunton 3y ago
Which country has such systems?
454.
by staunton 3y ago
It seems, however, that AI development (as opposed to what automation has been doing so far) will to a large part affect higher-income jobs. Your examples are "old-school automation" and don't involve AI. It's quite poss
455.
by staunton 3y ago
> it has been designed for verification from the ground up. It has a lot of places where you assume things work in a certain way and a lot of ways to assume it (and you can prove `false` if any of those assumptions aren't correct)
456.
by staunton 3y ago
A more experienced CEO would have come out ahead of the result Altman got, how?
457.
by staunton 3y ago
I would strongly assume Buzzard believes those two positions to be perfectly compatible and consistent. I'm sure it would be very insightful to hear him explain how they are. Hope someone asks him about it. > formalization would be
458.
by staunton 3y ago
Anyone who supported the board was in a situation where they deemed they could afford to go against the peer pressure. This is a combination of acting according to their beliefs/values and economic security. Those people should be envi
459.
by staunton 3y ago
> MS is still evil All big corporations are "evil", as in, their decisionmaking is scaled and institutionalized enough to effectively implement the goal of "maximizing shareholder value" above what's good for you
460.
by staunton 3y ago
That's actually quite interesting. I hadn't read the entire presentation, to be honest. Maybe it's a case of communicating priorities differently to different stakeholders... After all, it's about what the primary moti
461.
by staunton 3y ago
Here's people who are working on Lean's Mathlib discussing this https://leanprover.zulipchat.com/#narrow/stream/270676-lean4...
462.
by staunton 3y ago
Of course there's mistakes in papers. It's not that avoiding them isn't the primary motivation for formalization because they don't happen . It's not the primary motivation because mistakes in math papers happening
463.
by staunton 3y ago
I think porting automation will eventually solve this problem. It's really easy to write "amazingly good test-suites" for this stuff. So a computer will do the porting and you essentially "only need to read mehod signatu
464.
by staunton 3y ago
> what excuse do mere mortal mathematicians have? As an ardent proponent of formalizing proofs, I still have to disagree with this framing. Mortal mathematicians don't need any excuse not to formalize their stuff. They rather need
465.
by staunton 3y ago
Any anecdotes you can share? Also, I meant "make sure" in a negative way. As in you "make sure things are statistically significant" by e.g. p-hacking. Not that this isn't done in science but I think you're mor
466.
by staunton 3y ago
Yes. GR does it and GR gives good descriptions for a lot of observed phenomena.
467.
by staunton 3y ago
What do you do with it? Especially that benefits from Revise?
468.
by staunton 3y ago
That only concerns the time needed to implement it though, not capabilities. If an AI is known to be significantly better at diagnosing than your GP, and you know and believe this (this of course has yet to happen and then take time to be n
469.
by staunton 3y ago
Useful Full-Self-driving is arguably harder than "useful automated medicine" in two ways. First, you need insane reliability to match human performance. Much higher reliability than doctors even. Second, it's not "just&q
470.
by staunton 3y ago
It's possible most publicly available models (or at least "models the general public uses") will eventually refuse to give medical advice
471.
by staunton 3y ago
> statements like this literally set me off. The patient being right and the doctor ignoring the patient and treating the patient like an idiot There's a huge number of people who vastly overestimate their medical knowledge, google
472.
by staunton 3y ago
The magic words here are make sure .
473.
by staunton 3y ago
Going even further, deadlines are often a tool for signaling "the organization is trying really hard to achieve this fast". The shorter the deadline (as long as it's at least somewhat in theory plausible), the harder you&#x
474.
by staunton 3y ago
Illegally bribing someone is different from legally and secretly using money to influence the actions of institutions
475.
by staunton 3y ago
I'm not sure how Revise would work with a notebook though... Guess it's only useful in the REPL, which is a different way to work.
476.
by staunton 3y ago
That's getting much better since they started caching compiled code. With more software (and hardware, and synergy-between-them) improvements coming, this will soon no longer be an issue.
477.
by staunton 3y ago
And reinforcement-train an LLM to reconstruct the original code...
478.
by staunton 3y ago
Let's see how you do those high energy physics simulations with JS...
479.
by staunton 3y ago
> Pluto.jl does solve the state problem of notebooks Yes it does, unless you do crazy stuff (which you probably should put in a Julia file and let it precompile). The order of cells and execution order does not matter (unless you do craz
480.
by staunton 3y ago
What's the problem when working without REPL/notebook? The debugger IDE support will be fixed eventually™ (I really think it will.. eventually...). What else is there?

More ›