bollu

That's untrue. There are type-systems and type-checkers which can check for correctness, as specified by a mathematical formula. This is proof assistants such as Coq[1] work. For example, take a look at fiat-crypto [2], a project that generates code that is correct by mathematical proof, and is now deployed in Chrome. Another famous example is the CompCert [3] compiler, a C compiler along with a correctness proof that the compiler generates assembly which correctly simulates the C semantics.

These are based on powerful types as "dependent types" which can encode mathematics and programs in the same programming language, and allow the mathematics to "talk about" the program. The mathematical underpinning is the Curry-Howard-Lambek correspondence.

[1] https://coq.inria.fr/ [2] https://github.com/mit-plv/fiat-crypto [3] https://compcert.org/ [4] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

Nice explanation, I hadn't t heard this perspective, and it makes it a lot more intuitive! What's your favourite way to learn queueing theory? I feel like I'll get cool insights from this :D

Can you point me to a paper from the 70s that explains how to flatten such calls? The best that I know is "stream fusion, to completeness" which was published in something like 2019!

Could you name some pointers that I should look up to learn more about both sides of this debate?

I'd like a reference for this explanation :)

Do you have any recommendations to learn about how tropical geometry is used for control theory?

I don't believe that my individual choice actually matters; What do I read to change my opinion?

Where can I read more about how 72pt ~ 1 inch? Where does one g to for a "course on typography"?

What is the tool that builds this literate source view from source code?

I began to write an acerbic comment at "everything is a spring". I then thought about it, and realised you're so right. Linear algebra is crazy. Thank you for the insight. (It struck me that all of quantum mechanics I've ever studied in university was about learning to solve more sophisticated harmonic osciollators.)

I LOVED reading the culture. I'm still working my way through the books. They're eminently quotable. Here are some of my favourites:

> “Empathize with stupidity and you’re halfway to thinking like an idiot,”

> It would have helped if the Culture had used some sort of emblem or logo; but, pointlessly unhelpful and unrealistic to the last, the Culture refused to place its trust in symbols. It maintained that it was what it was and had no need for such outward representation.

> Just as it could not imprison itself with laws, impoverish itself with money or misguide itself with leaders, so it would not misrepresent itself with signs.

> So it had effectively frozen its primary memory and cognitive functions, wrapping them in fields which prevented both decay and use. It was working instead on back-up picocircuitry, in real space, and using real-space light to think with (how humiliating).

> Originally Damage was played on such occasions because only during the breakdown of law and morality, and the confusion and chaos normally surrounding Final Events, could the game be carried out in anything remotely resembling part of the civilized galaxy; which, believe it or not, the Players like to think they’re part of.

I hope this coveys the texture of the books. I have more quotes collected at my blog.http://bollu.github.io/quotes-from-the-culture.html

I only learnt the (arguably) "real meaning" of the Jacobian once I studied differential geometry. I haven't seen this explained anywhere. I took a stab at an elementary exposition (with animations) of this view of the Jacobian as the object that tells us how to map tangents from one space to another!

> No it won't

We don't know either way. relationship between BPP, BQP, P, NP are all open.

I am sorry. I shall reference Singular in the future whenever I discuss SAGE. Thank you for your fantastic work on Singular :)

Good question. I mostly use it for algebra. It has varying levels of support for analysis. There is a SageManifolds project that allows for computations over differentiable and Riemannian manifolds, for example.

Thanks! I'm studying this right now, after I got a taste of algebraic geometry (schemes) from Ravi Vakil's fantastic "algebraic geometry during the time of COVID" last year!

Also, use computers! I use SAGE extensively to get a feeling for lots of mathematical objects!

1. Grobner bases: http://bollu.github.io/computing-equivalent-gate-sets-using-...

2. Localization: https://github.com/bollu/bollu.github.io/blob/8cd335687ff3ef...

3. More broadly, an answer on math.stackexchange on how to debug math: https://math.stackexchange.com/questions/1769475/how-to-debu...

4. (WIP) continued fractions to compute pi: https://bollu.github.io/fractions/index.html

And so forth. I find the computational aspects of most theories to be very rich, and it's really gratifying to code something up and "read off" the results.

Thank you for the reference!

What's interesting textbooks andectures one can read on plasma fluid dynamics?

Fascinating! Could you tell me more about who these optimal users are? Are they optimal because they are the most valued users in their firms? (Make the best trades or some such?) are they optimal as their opinion on the software matters a lot? Or something else entirely that I am failing to imagine

That's a very cool connection I'd never thought of before, that IID random variables correspond to "maximamal local instability". What's this perspective called so I can read more about it for my interest?

What is free expression and where can I read more about it?

Do you have more on how to get better at writing?

Interesting, I'd love a book recommendation :)

What do you mean by "derive" the Schrödinger equation? As best as I know, there is no "derivation" beyond some analogy with the classical wave equation. It's an equation penned down by Schrödinger, motivated by the classical wave equation and insights from de broglie's theory.

I'd love to see a derivation if it exists.

That's not how it works, though. We can study any set of axioms we want. Mathematics often study "multiple incompatible worlds". For example, euclidean space where parallel lines never meet, and projective space, where parallel lines do meet at infinity. This is a general theme of math; we can study different sets of "beliefs" when we don't know which one is the "correct belief".

Thus, we come out on top, since we know what happens in all possible worlds.

I really do believe this, and the project of classical liberalism as a whole. However, I've found myself without a good response to:

> But everyone is biased, including journalists. So the best we can do is to get rid of the false narrative that journalism can be descriptive, and simply embrace the prescriptivist journalism-with-a-slant.

My gut tells me there's something wrong with this, but I can't spot what. I'd be enlightened if you can point out the problem with the above perspective

How precisely does one "leave their country for good"? Do you seek asylum? You can't actually just hop on a flight and go live someplace else without a visa, and that takes months to process.

What is "Rally"?

I'd love to read more about this, could you elaborate!