Time to break out John Baez's checklist: https://archive.org/details/TheCrackpotIndex
1,837 karma · joined October 13, 2010
https://cscheid.net https://github.com/cscheid https://bsky.net/profile/cscheid.net
Wirth was such a legend on this particular aspect. His stance on compiler optimizations is another example: only add optimization passes if they improve the compiler's self-compilation time.
Oberon also, (and also deliberately) only supported cooperative multitasking.
> Saying nature is mathematical is just saying that nature is consistent in the laws it follows.
It's more like "wherever nature isn't mathematical, we don't think about it as being mathematical", so saying "nature is mathematical" is very strongly tautological.
It's the same kind of situation as "why is everything linear?", or "why is everything an oscillator". The answer is more like "the things that aren't can't be easily described mathematically, and so we don't. What shakes out is mostly linear or quadratic (oscillators)".
You're right that typst is _very good_ at extensions, and likely will always be superior to quarto when it comes to that. The fundamental advantage typst has is that it's a "greenfield" project, and a very well-designed one at that, especially when compared to TeX.
> Looks like there are extensions that can be programmed, but they are more like second class citizens that you are not suppose to use normally.
We take quarto extensibility pretty seriously! "Simple" customization is available without need to program extensions, mostly through metadata configuration and classes and attributes in the document. This covers the basics like CSS, layout, document listings, etc.
For slightly more sophisticated extensions, you can create "filters" that operate directly on the document AST, either using the built-in Lua extension API or reading/writing a JSON representation (these are both built on top of Pandoc's capabilities, which quarto leverages extensively).
For reusable, packageable functionality, the extension system as it exists today is simple but certainly meant to be used "normally". It's how custom formats (the common, concrete use case is to provide different styles for particular academic journals) are defined and used.
That's how I ended up working there. 33T used to be packed full of gear but everything shrank so much that AT&T found themselves with dozens of empty floors. They didn't renew a lease on a big NJ lab I worked on, and a number of us ended up being able to choose commuting to NYC.
Not so fast; it could be done on a _different automated system_ (say, a smaller one) than the one you're building, in which case you're now relying on that system's correctness. Or it could even not be proven at all. This is not too different from what mathematicians do when they (often) say "assuming P != NP", or "assuming GRH", or "assuming FLT", etc etc. It's simply that it's worth being careful and precise.
> If a program is accepted by the proof checker, then by construction it must be a valid mathematical proof.
I'd phrase it as "If a program is accepted by a _correct_ proof checker, then ...". That makes it clear that we can't escape having to consider how and why the proof checker is considered correct.
Edit: this is not entirely academic. from what I understand, the unsoundness of Hindley-Milner in the presence of polymorphic references was not immediately known (https://en.wikipedia.org/wiki/Value_restriction#A_Counter_Ex...).
This is 5h of a single video from EWR to SFO by a former colleague. Turns out even a dumb trick like this still is enough to pick out a bunch of geographical features!
I don’t know about baseball cards, but the way Wizards of the Coast handles their policy around rare Magic: the Gathering cards makes me think their lawyers are definitely concerned about this kind of stuff.
A small suggestion: when you press the purple buttons, it would be neat to see the green numbers change by the multiplier (or have an option to do so). This would let you easily see parts of the keyboard transpose correctly vs not, and what new pitches you get access to. Even sweeter would be a quick animation to show "where the numbers went".
I would also like to be able to have the purple buttons be active only when pressing the keys, so that I could quickly modulate up a just fourth and back. Having to remember where I am in the modulation state is a bit much, and very different from typical musical instruments.
But I've been playing with this for a good while, trying to recreate basic stuff like V7 -> I etc and it's very cool, thanks again.
Yes, I wish so too. For what's worth, I'd buy "either of Dan Ariely and Francesca Gino write a NYT bestseller book in 5 years, go on a redemption tour, and nothing new happens" for $0.80 on a prediction market.
Fuck. These. People.
We put so much work making sure the analysis is right. Sweat the design, sweat the data collection, the consent forms, and dropped the studies where the result wasn’t there, as well as reporting null results. I specifically remember having to have a terrible conversation with a phd student that, after doing a power analysis, setting up a pilot study, and collecting enough data, we got p=0.054 on the relevant test. “Sorry, we can’t add additional participants; we can’t try a new analysis. We did the right thing and we should report a non significant result. It sucks.”
And these fuckers just go ahead and forge data to land TED talks?
Yes, let’s also have a conversation about incentives and the system. But individually, I reserve my sympathy for better people. Salt the earth they walk on, and rake them over coils. This is beyond reprehensible. Fuck. Them.
What choice? I have to fix bugs today as they come.
Not my business to decide what you think is reasonable. That's just what happens in the world, and what (in my view) good engineers sign up for.
I think you're assuming more of my answer than what I gave. That's fair given that this is the point of the article, but it's not mine. I'm very specifically only responding to "is there a per-user marginal cost on software?", and my answer is most definitely yes.
To warrant a recurring payment business model, I think the right question to ask is "Is there a per user-year marginal cost on software?", and now the answer is in my view, much more complicated and domain-specific. Worse yet, I think that there's perverse incentives at play here in recurring payments.
It's a bug in the processor that causes a bug in the software. It's not a bug in your idealized mathematical model, but try telling that to the people who paid you not to leak private keys.
I see my job as an engineer to be to create a product that satisfies the user's expectations (which in this case are eminently reasonable). It matters not one bit that I can point the finger to the chipmakers. I'm still selling something that I now learned doesn't do what I said it would. It's still on me to fix it the best I can. If I care about the product quality, that is.
_very different_, when the user's environment is different. And 1) you haven't seen shit if you think you can perfectly control the user's environment. 2) every new user is a chance for the environment to bite you.
> Do they make the product unprofitable or unsuccessful in anyway?
You do your engineer best to try and fight that. But there's absolutely a marginal cost, which is what I was responding to.
I don't believe such software exists. (And, to be clear, I'm writing from direct, day-job experience.)
EDIT: I take it back. SQLite, cURL. Maybe.
EDIT2: I can't reply to the SEL4 response, so here goes. I'm a huge fan of verification tools, but consider the Spectre class of bugs. Verification is always done wrt a mathematical model that you've defined after inspecting the world and writing down the properties you want to track. But the world changes, and the chance that the world changes increases with the number of users of your software. That's the nature of the beast.
Maybe you've never experienced the difference between writing software for 1000 people and writing software for 1M people, or (I imagine) 1B. The marginal per-person cost of software is not on shipping. It's on "what kind of weird shit will I now have to do because 1M is a lot of chances for my software to break weirdly, and people have paid for it"
> You don't have to worry about quality control and returns.
You don't have to worry about quality control and returns if you don't care about quality control or returns.
> Little context sensitivity
... this is close to a disqualifyingly wrong statement.
(I literally work with Markdown on a daily basis as my actual day job. Markdown really does suck.)
The only way in which (La)TeX is not context sensitive is that it's sensitive to the entire global TeX state at all times. There's no notion of grammar in TeX, _at all_. It's hard to trust the rest of the content in there after this.