There are incomplete parsers that cover most of the Org basics. For example, GitHub has one, crafted in Ruby. They use it to render e.g. readme.org files in repositories. It works quite well. I find the Org format very pleasant to work with.
I think the trick with Emacs and Org is to stick to the basics and then only add features or change your configuration very slowly, as needed. I have been using Emacs non-stop for >20 years and my .emacs is just 20 LOC. It's been shrinking, not growing. My goal is to bring it down towards 0 LOC. I have committed a few things upstream to modernize defaults.
Personally, I think the reputation of Org, Emacs, or Nix being hard and complex is undeserved. It's rather a documentation problem. There's no simple documentation to onboard newcomers and show them the basics in a principled way. So it looks like a mess, but it isn't.
> I have been using Emacs non-stop for >20 years and my .emacs is just 20 LOC. It's been shrinking, not growing.
Me too. I mean I'm using Emacs too, and it is 20+ years. I hate it deeply, and I cannot stop hating it because I cannot get away from it. I regret deeply choosing emacs 20+ years ago and spending 20 years to wrap my habits around it.
BTW my .emacs is still growing. I don't know how you manage to have 20 LoC of .emacs, I have a directory .emacs.d and a couple of dozen of files there. They are not large, some of them can be as small as 1 line. The last one I've wrote was dealing with indent of lua code. lua-ts-mode have some relatively simple rules that mostly work, but I was not happy with the result, there are some quirks that just are very inconvenient, and in some cases lua-ts-mode just fail to indent properly. So I fixed them to my taste. This one file is longer than 20 LoC.
Though, I should note, that LLMs make this much simpler. It is very simple to reverse-engineer what there is, and if you can explain the idea how to change the code, LLM can write all the elisp needed. It doesn't work out of the box, of course, and needs to be debugged, still LLM can save an hour or two.
> My goal is to bring it down towards 0 LOC.
You cannot. If you use lua you just cannot, because lua-mode uses indent of 3 spaces. Not 2, not 4, but three. So any lua sources you can find on github and try to edit will not be indented like lua-mode does. I cannot imagine what was going on the mind of the person who had chosen this value. The only possible explanation I have is something like "I want to be not like the others", but it doesn't seem right.
So you need at least to change lua-indent-offset (or lua-ts-indent-offset if you use treesitter), and it will be more than 0 LoC.
Thou shalt indent to three, no more, no less. Three shall be the number thou shalt indent, and the number of the indentation shall be three. Four shalt thou not indent, neither indent thou two, excepting that thou then proceed to three. Five is right out. Once the number three, being the third number, be reached, then compose thou thy Holy Lua.
You could customize that variable instead, so that Emacs manages everything for you and you don't have to care that it would look like a line of code if you opened your settings and edited them directly.
Yes, there are some parsers around in languages other than elisp. This one seemed to work well when I tried it some time ago: https://github.com/rasendubi/uniorg
As a heavy user of formal methods, I think refinement types, instead of theorem proving with Lean or Isabelle, is both easier and more amenable to automation that doesn't get into these pitfalls.
It's less powerful, but easier to break down and align with code. Dafny and F* are two good showcases. Less power makes it also faster to verify and iterate on.
Completely agree. Refinement types is a much more practical tool for software developers focusing on writing real world correct code.
Using LEAN or Coq requires you to basically convert your code to LEAN/Coq before you can start proving anything. And importing some complicated Hoare logic library. While proving things correct in Dafny (for example) feels much more like programming.
In EU/UK, some are sadly app only. I avoid those. Many others are pushing apps as a 2FA, even if you use their website. You need to insist to get another authentication system, like TAN. Some governments are also pushing mobile IDs.
The best Linux for phones, SailfishOS, has a fairly good Android compatibility layer that runs many bank apps well. But despite that, it's an uphill battle. The network effect of the duopoly is gigantic.
Lean is great, but if someone's primary interest is SWE, I think there are better choices. The Lean community is primarily focused on formalizing mathematics right now. This might change in the future. Lean is nice to learn theorem proving, but once you learn the basics, you'll hit a roadblock when trying to move to software verification applications.
For SWE, the most mature option is probably Isabelle. It's also a classical theorem prover, and it's perhaps easier to start with something that doesn't have dependent types. A cool thing is that the canonical Isabelle book [1] has been rewritten in Lean [2].
If verification is the goal, but you don't want to learn theorem proving yet, Dafny is really approachable and practical [1]. F* is also worth considering as a proof-oriented alternative to Isabelle that is focused on software verification [2]. Why3, Rocq and Agda are other obvious contenders.
The future is now. The recent couple of Lean releases have leaned more on software verification, I believe in part due to Amazon hiring a number of the core devs.
Maybe it's my own bias (after working for a big tech company for 5 years), but it's certainly not the dream job I thought it would be. Soulless corporations with questionable impact on society, lot of turnover, increasing pressure every year, fear of layoffs. Even the tech isn't that exciting, there's lots of tedious work, technical debt, hacked solutions, no time for researching and building quality solution.
That being said, it's certainly different for researchers. I can imagine that being a researcher at Google is more fun than being a median SWE in another FAANG. But still, I find these companies less enticing in general, even the products tend to degrade as they keep pushing the monetization.
I’m an ex-industry researcher with experience at FAANGs, albeit as a software engineering intern (Google) and a production engineer (Facebook).
I think it depends on the interests of the researcher. If a researcher is comfortable being a “brain for hire” who is comfortable solving research problems that are driven by business needs and where there needs to be short-term or medium-term results, then I think there are plenty of opportunities at large companies, including the FAANGs. I find research more fun than software engineering, but researchers are far from immune from pressures to ship.
If a researcher is more interested in curiosity-driven work and who wants to work on a longer time frame, I’m afraid that there’s no place in industry, except for maybe Microsoft Research (which I’ve heard changed under Satya Nadella), that supports such work. The days of Bob Taylor-era Xerox PARC and Unix-era Bell Labs ended many decades ago, and while there were still curiosity-driven labs in industry well into the 2010s, I have witnessed the remainder of these old-style labs change their missions to become much more focused on immediate and near-immediate business needs.
My experience as an L5 Google Research research scientist is that I have a lot of freedom as long as I can show I've made progress on one or two things the company cares about at each annual review. IMO, this is about as much research freedom as is reasonable for me to request.
Land cruisers are almost collectors items now in the Middle East. Transcends across wealth and status. Doesn't matter if it's a middle class office worker with a large family, a soccer mom living in the Palm or a filthy rich oil sheikh with an arsenal of sports cars stored away in his garage - they all have Land Cruisers (or the Prado).
I might actually just get into the hobby of collecting Land Cruiser models, and maybe a few Japan-exclusive Toyota models.
Progress with RL is very interesting, but it's still too inefficient. Current models do OK on simple boring linear code. But they output complete nonsense when presented with some compact but mildly complex code, e.g. a NumPyro model with some nesting and einsums.
For this reason, to be truly useful, model outputs need to be verifiable. Formal verification with languages like Dafny , F*, or Isabelle might offer some solutions [1]. Otherwise, a gigantic software artifact such as a compiler is going to have a critical correctness bugs with far-fetched consequences if deployed in production.
Right now, I think treating a LLM like something different than a very useful information retrieval system with excellent semantic capabilities is not something I am comfortable with.
I think the trick with Emacs and Org is to stick to the basics and then only add features or change your configuration very slowly, as needed. I have been using Emacs non-stop for >20 years and my .emacs is just 20 LOC. It's been shrinking, not growing. My goal is to bring it down towards 0 LOC. I have committed a few things upstream to modernize defaults.
Personally, I think the reputation of Org, Emacs, or Nix being hard and complex is undeserved. It's rather a documentation problem. There's no simple documentation to onboard newcomers and show them the basics in a principled way. So it looks like a mess, but it isn't.
reply