artagnon

Ruby.

I still love the language, and maintain my SSG that was written in Ruby over a decade ago. Shame that it's nearly dead now.

LLVM deprioritizes helper scripts such as update_analyze_test_checks.py, and the build infrastructure is far from perfect. Scripts like the ones categorizing PRs are very much unpaid work.

LLVM also deprioritizes general cleanup work, such as getting rid off passes that don’t work, and are rotting in the tree: of the top of my head, I can think of GVNSink, LoopFusion.

There are additional problems unique to LLVM, as it doesn’t have a dictator: there are multiple different dependence analysis in tree, for instance.

This echoes the problems we see in LLVM. Tooling is de-prioritized in several large corporation-funded open-source projects.

LatexML has come a long way. Even arXiv uses LatexML internally to offer HTML5 versions as of late 2023. It does have limitations in not supporting all packages, or producing a high-quality translation in all cases.

If you don't need to convert entire LaTeX documents, MathJaX and KaTeX are really good at rendering a subset of LaTeX as MathML/SVG. I run MathJaX + an xypic extension for commutative diagrams with server-side rendering on my website, and it works great in practice.

It's standard MathJaX that's rendered client-side. I managed to get MathJaX + XyPic rendered server-side on my website, which is a lot nicer.

Oh no! I think we’re out of luck if my reading of [1] is right. Sonos API only supports streaming from a single URL.

[1] https://docs.sonos.com/docs/streaming-basics

Very slick interface with a nice selection of sounds! I would definitely use this if only it could connect to my Sonos.

Honestly, everyone working with C++ sticks to a select subset of the language that they've chosen for their project, or the project they're contributing to. Nobody knows all of C++. Personally, I don't mind C++ forking out in different directions and accepting diverse proposals; while I wouldn't bother to use them myself, I realize that it may be useful to other people.

C++ is an engineer's language, and it's ridiculous to imagine that we'd ever need a C++2.0 that cleans it up. Subjectively, you could say that some features are "ugly", but this is an evolutionary process, and there are bound to be vestigial features.

Yes, there are memory safety issues, but in practice, these are isolated in very few places. Take a compiler like LLVM for instance: most developers are working on transforms or analyses, and they're exposed to zero manual memory management. Sure, the Pass Manager needs to build passes, and the IR needs to be allocated, but that's about all the manual memory management there is.

Personally, I couldn't care less about standardized argv-parsing, as each project has its own set of complex requirements. There are JSON parsing libraries available for C++, and I don't see why it should be standardized. Faster hashing in std could be a low-priority feature, but projects like LLVM have their own optimized version of std data structures and algorithms.

I suppose a module system could be useful; most C++ projects are built with CMake which is already very good at finding and linking dependencies. Personally, my biggest pain point is compile-times, but that's really an LLVM/Clang problem.

Overall, the article doesn't seem to be written by someone who has a lot of experience with large C++ codebases.

God, this is so dehumanizing. When I think about the places such a thing can possibly happen, I think of North America and third world countries.

The example described in this post is JSON parsing in Haskell, but I've implemented a complicated compiler transform that lifts loops to static control parts (SCOPs), in the past, in C++. Each inner function in the lift would switch on valid constructs, either returning a lifted integer set, or throwing an exception on match failure. Although exceptions have a non-trivial cost in C++, it was the cleanest design I could come up with at the time.

Is tree-sitter really slower than TextMate grammars? Some benchmarks indicate that this isn't really the case [1]. On the other hand, breaking parse trees is a real issue, because the error-recovery in tree-sitter is pretty rudimentary [2][3], but as you said, it's not an issue for Shiki.

Several TextMate grammars suffer from inaccuracy bugs, and issues of maintainability. Perhaps the biggest hindrance in the adoption of tree-sitter, is that the most popular editor, VSCode, still doesn't support it.

[1] https://github.com/microsoft/vscode/pull/161479

[2] https://github.com/tree-sitter/tree-sitter/issues/1870

[3] https://github.com/tree-sitter/tree-sitter/issues/224

Unfortunately, even the LLVM community has chosen a combination of Discord/Discourse, and deprecated their mailing list/IRC channel. This is a very unhealthy trend, and only the most ardent of communities such as Linux/Git/GCC stick to old-fashioned publicly-archived mailing lists.

[1] https://public-inbox.org/README

Hehe, perhaps when I'm older. My collaborator on the LICS paper also tells me that the countryside is very beautiful. It will take time to get used to, as I've lived in big cities for the entirety of my life, and participate in activities like book clubs.

I initially kept that option open, yes. However, there are surprisingly few available positions in formal methods outside of academia, and Coq is very very hard: my ability to prove things with Coq is quite modest.

Probably worth noting that I did have an PhD offer earlier, to work with Coq. However, since it was in a small village in Germany, I had to turn it down.

On a more general note, I don't know if formal methods is that promising today: proof assistants are very immature, and proving even little things involves a lot of trial-and-error and is very time-consuming.

Yes, I recall interacting with you!

It's less a question about what changes, and more a question about how well you can recall your past experience (I had the big picture, but forgot the details of several optimizations I'd written in the past, as well as certain CS fundamentals), and how well you can do online coding interviews (I've only written Coq, at a glacial pace, over the last three years).

I will mainly be working on the middle-end and back-end for RISC-V.

I used to work as a compiler engineer in the US for several years, before deciding to try starting over at the age of 30, in pure mathematics. I moved from the US to Paris in pursuit of an affordable mathematics education, and spent two years in a Masters program. I did have a considerable amount of savings, but it was very risky nevertheless: if it didn't work out, I'd be out-of-touch with compilers, and it would be hard to interview again, with a considerable career gap in my résumé.

For various reasons, mathematics didn't work out, and I was forced to interview again. Fortunately, I did manage to find a job as a compiler engineer again, and will be moving to London soon.

Now, the price of my adventure was quite steep. I uprooted my life when I moved from the US to Paris (especially because I didn't know French at the time), and the upcoming move to London will once again be difficult. I nearly halved my savings, by studying mathematics at my own expense, and will be back to earning the equivalent of my starting salary in the US.

However, I'm an adventurous person, and view my experience in positive light. I'd been wanting to study Jacob Lurie's books for the longest time, and I finally did it. I worked on a mathematical manuscript, which is now up on arXiv [1], and on a type theory project which has been submitted to LICS '23 [2]. I've had a good life in Paris, and my French is decent.

There's the larger philosophical question of "What is a life well-lived?", and for me, the answer is to pursue those things that you're truly passionate about, even if it doesn't work out.

[1] https://arxiv.org/abs/2211.09652

[2] https://artagnon.com/logic/νType.pdf

I think Lua was always seen as a bit obscure, and not enough people invested in the language to write useful utilities. It has a solid C foreign function interface, and the compiler is quite fast, which leaves me puzzled about why it never gained traction. I think it's an embedded scripting language in the majority of use cases (e.g. NeoVim, LuaLaTeX, scripting in some game engines).

The story of Ruby is altogether different: they made the fatal mistake of not defining a C foreign function interface in the standard, otherwise I imagine we'd be seeing numerical computation and ML libraries with a Ruby interface today. Still, Ruby lives on in Metasploit, and in Sorbet and Crystal.

It's interesting that Ruby now pulls Rust as a dependency, since YJIT is written in Rust [https://github.com/ruby/ruby/tree/master/yjit].

Sorry to be the buzzkill here, but I'll say what needs to be said. Computers are decades away from being able to formalize any serious mathematical results, and "formalized mathematics" is a fancy term for "formal methods in computer science".

I've worked for a good numbers of years in the US software industry as a compiler engineer, and am a Mathematics masters student now. I've played with proof assistants extensively, and in particular I'm currently working on a paper to formalize semi-cubical sets in Coq. Working with Coq has been most painful, and it requires spoon-feeding for verifying even the simplest results. Worst of all, it's riddled with bugs, and I'm constantly astounded at how stupid it is.

That said, Lean is a much newer proof assistant, and while it offers some nice conveniences, it will take at least a decade before its power is comparable to Coq.

Mathematics is a solitary activity for good reason. Much of the work happens on pen-and-paper, and it takes months of toil to prove a result. No serious mathematician is going to go through the pain of encoding her proof in a proof assistant, and spoon-feeding it to verify every little result.

What's the news? That several computer scientists in the area are doing the work of formalizing simple mathematical results in Lean. Don't mistake Lean for some ground-breaking new technology; sure, it has a thriving community, and offers many conveniences, but the level of abstraction it offers isn't even close to the level of abstraction that my subject offers (I study stable ∞-categories).

Sure, if you want to do the thankless work of formalizing well-known results from group theory, ring theory, or vector spaces in Lean, be my guest. But don't be under the illusion that it's going to change the way mathematics is fundamentally done. The work is comparable to type-setting a document, except that it's a LOT more painful.

KaTeX doesn't do commutative diagrams, unfortunately.

Outputting beautiful designs is a function of the css, no? The bundled css is quite minimalist, and it comes packaged with a relatively simple starter website.

Yes, it's not the fastest ssg; there's Zola for that. However, digging git history with `git log --follow` can take a moment, and the MathJaX server-side rendering takes 10 seconds on a math-heavy site. However, incremental builds are the default, and a full-rebuild is seldom necessary. What makes it beautiful is the following:

1. You don't have a metadata header, like in most SSGs; timestamp is picked out from git-history, and topics/subtopics is simply picked out from the folder structure.

2. The syntax is terse, and features like un-numbered lists is excluded on purpose, because mathematicians like to number or letter everything.

3. The implementation of claytext is simple. There is no complicated markdown-processing, and even hard-wrapped lines are not allowed.

4. There's a dedicated vscode extension for auto-completing MathJaX. It also triggers a build-on-save, so you can just save changes in vscode and refresh the browser to see the changes.

5. Server-side rendering of math, so that the client isn't burdened with executing heavy javascript. It actually uses a custom fork of XyJaX to achieve this for commutative diagrams.

To formally verify simple things where a simple SMT solver does the job, why do you need a 40-year old beast like Coq? Even the very title of the article doesn't make much sense: why would you _want_ to translate Z3 to Coq? Coq is useful, not just for formally verifying things that are far more complicated, but also for formalising (simple) pure mathematical constructs (ref: the HoTT effort). Coq was used to formally verify an entire C compiler (ref: CompCert), which was a landmark achievement.

If you're looking for a middle-ground between SMT automation and proving things that automation fails at, see efforts like F*. There are several proof assistants that use Z3 as a backend.

Coq is the oldest and most mature proof assistant. There are simpler alternatives like Agda, Isabelle, and Lean, each with their own downsides for the simplicity that they offer. For instance, cubical type theory has been formalised in Agda, but I'm currently working on a project to formalise semi-cubical sets in Coq, a project that has been running for a year, and might not be completed.

Coq has a very advanced dependently-typed system, but as a result, the Coq unifier is heuristic-based, and fails at certain points without good diagnostics. That's where the Coq tactic system Ltac2 steps in: there is no other proof assistant that has such such an advanced tactic language.

TL;DR: Coq is a 40-year old ageing beast, and there is nothing quite as powerful. However, even it is immature when it comes to formalising higher categories or other similar graduate-level mathematics. It's painful to work with, because of the number of warts it has accumulated, but there is simply no alternative.

Fwiw, I've lived in New York, Boston, and the Bay Area too. Four and a half years in the US in total ;)

Yes, this is the unfortunate reality. It happens to the best of software as it ages. The article doesn't address the elephant in the room: MediaWiki is really the _only_ solution to a difficult problem that we have today. Which other markup language is so comprehensive? Yes, it's unnecessarily complicated, but let's understand that the constraints are very tight: the data can't be separated out of the markup, and it's impossible to make backward-incompatible changes. Many of the really great pages on Wikipedia render beautifully.

It's untrue that they haven't added features over the years: they have, but they do it at a glacial pace. Consider one of the recent ones: when you hover over a link, a box pops up and shows a preview. They used to render math on the client-side, but now, they just convert to SVG: as a result, it loads instantly, and renders consistently. The WYSIWIG editor rollout was slow, because people felt that it would attract low-quality low-commitment edits. They first released it as an optional feature, and then turned it on by default, when they were confident that it worked as intended. Oh, and my favorite? Allowing an article to start with a lower-cased word (say iOS); I remember that there were a bunch of redirects just to correct for this deficiency.

Yes, it is a giant pain to edit some pages in that arcane syntax, but nothing else even comes close in terms of features.

Yes, there are an enormous number of templates, but in practice, an infrequent contributor just finds a page that uses a similar template, and copies it out.

Yes, there are lots of bots, and they try very hard to guard against spam, without making you sign up or even solve a CAPTCHA to edit. Plenty of bot edits are "good" edits: they revert rage-rewrites, rage-deletions, and all kinds of malicious user behavior.

What you don't understand about redirects is that, the good ones can't be automated. It's not a string-matching problem. Yes, they could automate /some/ of the redirects, and they try. I've personally never run into a typo-redirect in recent years.

Yes, it can get political at times, and it's _very_ difficult to have objective guidelines about which pages are worthy of existing. Politicians' pages often get locked, when there's an upcoming election, and this means that you need an account to edit. Again, MW has lots of great features.

Wikipedia is aging, and nobody can deny that, but who would want to do the thankless work of parsing the markup and porting it to another system, AND correct the breakages? What commercial value does it have, and who's going to fund it?

The choices are still available; it's just hidden beneath layers and layers of commoditization. Gone are the days when we could grow our own spices. Not really: you just have to move out of the city, to a nice European suburb and you can have a garden. Gone are the days when we could forge our own knives. Again, not really. You have to move to some kind of village, where you have access to the local smithy. Let's talk about a trade-off that most people actually face: in the US, they drive in their oversized cars to a mega-super-market and shop for the week. In Paris, I go to my local bucherie for my meats, my local boulangerie for my breads, my local poissonorie for my seafood, and my local fruit and légume marché for my fruits and vegetables. I shop once every few days. It's a big deal for me. I get really high-quality food at good prices, with a personal touch. You'd lament about not having this choice in most parts of the US.

Yes, computers have reached a new level of commoditization. So much so, that many users just use a smartphone and tablet. It's a lot more convenient than sitting at a terminal and with a cherry MX keyboard. But those choices are very much available; they just aren't available to everyone. If you really wanted, you can even design your own processor die based off RISC-V designs. And yes, you can totally build your own Linux system from scratch: I'd argue that's there's a lot more choice available in this regard. Remember the days of the simplistic GNU Stow? Today, there's Nix, and you can base your entire system on it. And use XMonad, rxvt-unicode and zsh, if you so desired; they're still maintained, last I checked. I'm sure there are packages for eccentric people to design their own cursors. FreeBSD and OpenBSD exist, and are quite viable. You could even base a system on SeL4, if you're into that sort of thing.

I wholeheartedly agree that this kind of commoditization is actively harmful and stifles creativity. Cashiers and librarians are walled into their little interface; in the best case, they might figure out how to play a game of Freecell. It's sad, but this is the price we pay to put multiple little computers in everyone's hands. Choices create fragmentation, and with fragmentation, there's little incentive to keep fixing the bugs on esoteric fragments. Every choice increases the testing burden exponentially, and to avoid special-casing each combination of choices, software ends up being written for the lowest common denominator. The result is something like Linux on laptops today: the defaults are so terrible that you're forced to mess with the touchpad driver to get basic usability.

I've experimented with Soylent for almost 1.5 years, and here are my main takeaways:

1. It's far from perfect, but can serve as a substitute for junk food. After six months of switching to Soylent, the cholesterol in my blood had dropped significantly, as verified by blood tests.

2. It's much easier to moderate food intake with Soylent. If you eat out, especially in the US, the portions tend to be huge, and there's often a post-meal slump. Soylent makes it possible to continuously consume little amounts of food.

3. Your body loses the ability to process solid food if you have too much Soylent. It's possible to get addicted to Soylent, and develop an aversion for regular food, and this is unhealthy, to say the least.

4. Cooking and eating home-cooked meals is an essential part of overall well-being. For snacking on-the-go, smoothies are a good substitute. With yoghurt, seeds, and protein powder blended it, it's arguably healthier than Soylent.

Conclusion: Soylent is like one of those fruit juices you might pick up at the supermarket, when you fancy it. Getting cartons of it shipped home every month is harmful to overall well-being.

No, because my undergrad wasn't in math.

Chennai Mathematical Institute.

What seems to be the problem with CTRE?