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.
1,571 karma · joined March 2, 2009
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 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.
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.
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.
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
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!
I will mainly be working on the middle-end and back-end for RISC-V.
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.
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.
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.
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.
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.
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?
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.
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.