Unsurprised. I got the impression Bukele picked bitcoin in a sort of manic ADHD moment and no one pushed him on it, figuring it was their president’s personal indulgence.
Actually it was the for profit corporation that hijacked the Bitcoin GitHub repo a decade ago, Blockstream, that pushed the idea, Samson Mow specially is the one who deserves most blame.
I'm impressed with Devin's capabilities. Its good at building standard web applications and implementing common patterns. I is particularly effective for enterprises needing basic web pages or solutions that follow established development patterns.
While Devin handles routine development tasks well, it still requires oversight and guidance when dealing with complex integrations or custom business logic. It was helpful in reducing the time spent on boilerplate code and basic setup tasks.
The number N in question will adjust with dx (up to infinitesimal error anyway). So if dx is halved, N will double. But both retain their character as infinitesimal and hyperfinite.
But they don't retain their status as hypernaturals! dx does not need to evenly divide the interval over which the integral is taken. Whenever it doesn't, the number of slices in the integral will fail to be a hypernatural number, because one of the slices will extend beyond the interval boundary.
The theorem tells us that the area of the extended interval that uses a hypernatural number of slices has the same real part as the area of the exact interval. It doesn't tell us that the exact interval contains a hypernatural number of slices.
Yes, but that's also the entire thing I was questioning. The essay says that an integral necessarily contains a hypernatural number of infinitesimal slices. I don't think that's true.
There are theories like SPOT and Internal Set Theory that don’t require filters.
Plus the ancient mathematicians did very well with just their intuition. And more to the point, I cared much more about building (hyper)number sense than some New Math “let’s learn ultrafilters before we’ve even done arithmetic”.
> Plus the ancient mathematicians did very well with just their intuition.
They did. But they also got things wrong, such as thinking that pointwise limits are enough to carry over continuity (see here for this and other examples: https://mathoverflow.net/a/35558). Anyway, mathematics has changed as a discipline, we now have strong axiomatic foundations and they mean that we can, in principle, always verify whether a proof is correct.
Certainly I'm glad we have better tools now, and know the rules. Sure beats the old days. As for verification, well I'm big into Lean 4 and it plays well with NSA since transferring theory and proofs between finite and infinite saves a lot of labor on the computer.
Oh I wasn't trying to say that NSA is in any way non-rigorous, only that if you make it rigorous it does require some machinery that is itself not terribly straightforward.
As for whether that's worth it or not, I have no strong opinion.
Gives what you wished for. It's functional, though (among other things). Unlike most lisps, (dependently) typed. But hey, available at compile-time.