It’s security issues exactly like these (as well as a few other not mentioned such as package signing or possibly better SELinux support) that have kept us from investing in nix (government sector). Many of these types of things would need to be solved for us to be able to use nix in production.
For some of the issues like the current pull request model and packaging review I’m doubtful anything will change enough in the near term which is super unfortunate because of the potential nix brings to the table.
IMHO, thanks to its declarative nature, Nix is uniquely positioned to implement some user-friendly form of role-based access control and isolation. There are some efforts to support bwrap and AppArmor. SELinux is another option. I tried to push for things in this direction during some Nix meetings, but there are some really young contributors with zero engineering experience that think it is a bad idea because it’s incovenient and nobody uses it…
current pull request model
Great point as well. I am the official maintainer of a dozen packages and the current pull request model is a bit broken. Very often package source gets updated upstream. Nix bots update the source and create a PR for me to review. Typically, some other person rushes to push it without maintainer agreement. It looks like many GitHub users are trying to hoard many “contributions” to enhance metrics on their profile, which is valuable towards getting job interviews. This is scary, as malicious code can easily creep in.
Note that the PR and packaging reviews are for nixpkgs, not nix.
If you want different outcomes for nixpkgs reviews or a subset curated with better reviews and all, and have access to government money, i would recommend reaching out to the Nix foundation?
The main reason it is this way is that we are short of people to work on it. This is solvable with money. A support contract, signed with an org we would create for this purpose, is not an impossible thing to imagine.
If you want different outcomes for nixpkgs reviews or a subset curated with better reviews and all, and have access to government money, i would recommend reaching out to the Nix foundation?
I don’t disagree but pragmatically speaking it’s not that simple. For example, I’m one of two contractors on a specific team. Nix (the whole ecosystem) could provide real value to the struggles that we face daily. But using Nix in production, is an absolute non-starter at the moment due these style security issues.
Neither I, nor my team, have direct access to “government money,” we’re on a fixed contract. We also can’t just send money to sponsor work on nixpkgs. We need an actual organization that we can form a contract with for a billable service (basically all “purchases” above a particular threshold are actually contracts). i.e. Most of our infrastructure is RHEL and no-one bats an eye at spending many tens of thousands on RHEL support and subscriptions.
But it also seems like this type of offering is something the Nix community would absolutely oppose because it would require a non-community based org able to drive work and paid employees on timelines with SLAs, etc. Every time I see DetSys propose something it’s met with all kinds of ire about, “We can’t let nix be taken over by a corporation!” (there are lots of DetSys supporters too, to be clear)
Unfortunately too, it’s a chicken and egg problem at the moment. Even if for example the Nix Foundation (or whomever) started selling support contracts, we couldn’t immediately buy it because at present those security issues aren’t solved so we couldn’t yet put it in production. And if it can’t go in production we can’t purchase support. Additionally, being a community based project, there is disagreement on how, or even if the issues we care about should be solved.
So even hiring another contractor dedicated solely to nixpkgs isn’t feasible. Even ignoring the usual government red tap that makes anything take three times as long as you’d think (modifying a contract, requiring new bids, the convoluted hiring process, etc.), that one individual most likely can’t realistically affect the underlying security issues we’re talking about. Even nixpkgs review as others have mentioned, because unless somehow this new hire was able to instantly get merge rights their PRs would sit just like everyone else’s. Of course people will say, “Just hire someone already working those issues!” well, show me one of those individuals that has (or can get) a US security clearance, and is available for non-remote work in the US once a contract modification was approved in 12-18 months and I would genuinely love to talk to them! (Seriously…if that type of person exists I would be able to use them in all kinds of settings even if the nix stuff wasn’t viable).
It’s super frustrating down here where face daily challenges that we see a potential solution to.
Without deep inspection it’s often hard to tell whether it’s the browser/website, or network latency, that is causing any visible delay - it is possible that you might be ascribing e.g. JS execution time to “the internet” on some sites.
I guess it is possible, but then 9/10 everything works fast on the good Internet days. It is only when Internet is slow that I ever start to moan about how everything is slow on a computer.
I am not saying there haven’t been noticeable perf improvements in browser history.
However, I think we are a point of significant diminishing returns. I am struggling to imagine that we are going to get measurable (from consumer perspective) performance improvements moving forward.
Many years ago, I was at a talk by Robin Milner where he argued that artificial intelligence is the wrong goal and that we should focus on augmented intelligence. Making computers do things that humans can do is not especially useful, making computers and humans able to do things that neither can do in isolation is hugely beneficial. Things like Copilot fit well into that lens, they don’t replace the human they let the human accomplish more.
To the notes at the end, I don’t find it worrying that an LLM can reproduce college essays, at least in the sense that’s implied. I see this as evidence that these forms of assessment are not measuring the right thing. I hope LLMs will be a disaster for the kind of assessment that doesn’t require original thinking yet purports to measure that faculty.
I don’t find it worrying that an LLM can reproduce college essays, at least in the sense that’s implied. I see this as evidence that these forms of assessment are not measuring the right thing.
I agree. When these LLMs reach such high scores on standardized school/university tests, the shocking thing is not how far computers advanced, but how primitive our assessment of skill truly is. That it can be fooled by what amounts to a probabilistic mechanism that generates likely chains of tokens. That is not the kind of skill and resourcefulness you look for when you’re hiring people. True resourcefulness is navigating uncharted waters, not doing what is familiar but doing what is logical, given the circumstances.
It’s tricky. When you design an assessment there are four key things you need to think about:
Validity. Are we actually measuring the right thing? In the simplest case, are we actually measuring something: internal consistency metrics leisure this.
Reliability. Are our results reproducible? If the two cohorts of equal ability sit the same test, will we see the same distribution of results?
Impact. Does the thing that we’re measuring correlate with the thing that people looking at the test score care about? For example, if the test is a qualification used for getting a job or getting into university, does the test score correlate with your ability to do well after being accepted?
Practicality. Can we actually run this test at the scale necessary? Having an expert follow the candidate around for a few weeks while they demonstrate the skill works really well, but tends not to scale (especially if you want reliability, so have to calibrate your experts’ judgement).
A lot of university exams don’t even start with a construct against which they can measure validity. They have some aggregate hand waving towards impact (do people who graduate our course get good jobs and do well in them?) but often the sample sizes are too low. They do care about reliability because that’s the kind of thing that they need to demonstrate for accreditation, but only very loosely. They care a lot about practicality because the people marking assessments are not doing that full time, they’re also doing research.
Even with those caveats, a number of the things where LLMs do well are the kind of assessments that are intended to drive learning rather than give a final score. They are intended to tell the student what they need to study more. Cheating at these is like cheating at exercise.
Many years ago, I was at a talk by Robin Milner where he argued that artificial intelligence is the wrong goal and that we should focus on augmented intelligence. Making computers do things that humans can do is not especially useful, making computers and humans able to do things that neither can do in isolation is hugely beneficial. Things like Copilot fit well into that lens, they don’t replace the human they let the human accomplish more.
I wasn’t at the talk but I think I saw either a recording of it, or he made that point in a later talk that I saw, and it was a pretty defining moment for my outlook on programming, and on technology in general. Based on that, and on my personal observations, I also think rumours of programming being on its way to the urn because of “AI” (by which commenters usually mean LLM) are greatly exaggerated. This article is probably a good example: it has a few good ideas, but the examples are tone-deaf.
I don’t remember where I read it first (I think Norvig quotes it in his big book on the topic, but I mostly skimmed it – my interest in AI is mostly confined to writing things that allow people who are better at math than I am write AI tools) but at some point, someone noted that mankind finally achieved its ancient dream of flying when it stopped trying to emulate the flight of birds, and tried to make things that fly starting from the principles of flight but without attempting to emulate the form of flight.
The examples in this article miss that: they get hung up on code monkey “tasks” (which may ultimately be fixed by incremental progresses in LLMs; ChatGPT 4 fares better on a lot of things, who knows what ChatGPT 6 will be able to do) or pointless programming puzzles. With any luck, something good may come out of that, like the death of interview programming puzzles, but that’s IMHO that’s not where the potential of LLMs lays.
I’m (slowly – the web is really not my platform) writing a tool that uses LLMs for very practical problems. tl;dr wife runs a marketing agency, I’m writing a tool that assists with the analysis of various types of promotional text. It’s very much an analysis tool; it has an interface that vaguely alludes to virtual assistants but the interaction is not chat-driven at all.
After hacking at it for a couple of evenings I’m fully convinced that LLMs will not spell the end of programming, and I’m really enthusiastic about what they can do:
Getting that kind of analysis from a language model would’ve been absolutely impossible 10 years ago, and would’ve required concerted effort from several graduate students to come up with a very narrow model. Getting a very useful analysis (I’m talking things like identifying elements of marketing/sales strategy) is something I’ve been able to do with an investment of like thirty minutes, ten of which were spent yelling at Docker.
Turning that into a useful program absolutely requires programming effort. This isn’t something you can do with a no-code tool. You can get some of the output the program produces with nothing but the ChatGPT interface but it’s extremely unwieldy. Properly organising it and correlating various bits and pieces of output is not something a LLM can do, and being able to do it efficiently and repeatably – which is definitely done by old-fashioned programming – is a big deal.
The examples in the article are relevant in one way – I’ve found LLMs to be remarkably good at doing things that otherwise require tedious and somewhat “machine-like” human effort. For example, despite extracting and correlating a bunch of data from freeform text, and then showing it in standard format, my code has basically no serialization/deserialization logic. If I need ideas extracted from a text, and I need to hand them off in JSON format to the UI layer, I just request them in JSON format. If I need to show formatted text, I just request it in Markdown format. It’s not foolproof: chatgpt-3.5 occasionally hands me invalid JSON or tries to be nice and say “Here’s your JSON first”, so there’s some basic sanitizing logic in there; and there are security implications to it that I haven’t fully come to terms with. However, these look like problems that are perfectly tractable between incremental improvements in LLM (or, for that matter, some format awareness) and some real-life experience.
This part of writing an application may go the way of the Dodo – all that code that takes these two JSON objects and produces this other JSON object in a slightly different format, or takes this CSV document uploaded by the customer and produces this standard BOM table. But bloody hell, good riddance, if anyone dreads a future in which we’ll have to do less CRUD and object mapping, they’re suffering from Stockholm syndrome.
I think things could head in this direction? LLM-generated code is probably difficult to trust. There is some interesting work on synthesis based on contracts / advanced type systems using SAT/SMT. I expect both approaches might converge. We may end up designing programs, with AI helping to fill in the gaps.
Some things are. This is explicitly the goal of copilot. I am not convinced that it’s going in the right direction though because it’s acting as a glorified autocomplete and if typing is the bottleneck when programming then I’m doing something wrong. The kinds of things that I would love to see from LLMs are:
Give me LLM-generated code review comments, trained on code review comments fine tuned with my repo, before I push. Even if these have a moderately high false positive rate, if they can flag things that I should double check them they may be useful.
Natural-language-driven refactoring tools. There are a bunch of mechanical refactoring that I do that are easy to say but hard to automate.
Naming style checking. Clang format can do things like ‘this must be camel case’, but not things like ‘interfaces must be adjectives, classes that implement these interfaces should be noun phrases incorporating the interface’. That kind of thing would be fantastic for automated tooling to do since it’s one of the most time consuming things to get right in good APIs.
Automated flagging of APIs that don’t match (or, worse, almost match) design patterns used elsewhere in the library. This requires fuzzy pattern matching, the kind of thing that LLMs are really good at, but also requires quite a large context window. Humans are often bad at spotting this because their equivalent of a context window is smaller and doesn’t find the places where the library has exposed an interface that’s confusingly similar. I’m the simplest case, this can just flag the same kinds of parameters in different orders but there’s a lot more that it could do.
The main thing here is that they’re all low stakes: it won’t break the code if the LLM is wrong (except the refactorings, but that can be coupled with testing) but it will make the output much nicer for the same human investment.
assuming that the human brain is not the maximum possible intelligence a mind can have, and that artificial intelligences can surpass our intelligence by orders of magnitude, and that they can be run on faster processors with larger data stores, that AIs could be reproduced with a simple ctrl-v ctrl-p– the question should not be “what is AI good for?”, but “extrapolating current trends, how much longer will humans be useful for anything at all?”
assuming that the human brain is not the maximum possible intelligence a mind can have,
That is probably true, though it may be that it devolves into discussions about forms of intelligence. The human brain is an interesting balance of compute vs I/O and it may be that increasing compute power alone is not useful, increasing compute and I/O gives something that is unrecognisable. Given that we currently have a sample size of one for building models of kinds of intelligence, there’s a lot of margin for error in anything that we build.
and that artificial intelligences can surpass our intelligence by orders of magnitude,
That’s a nice hypothetical but no one knows how to build one that even reaches the level of a human yet. The article shows problems that young children can solve but that state of the art LLMs can’t. To exceed by orders of magnitude, they’d first have to reach parity.
That said, there are some things that computers can already do orders of magnitude faster than humans. They can compute the sum of a list of integers many orders of magnitude faster than humans, for example. A human with a spreadsheet can achieve far more than a human without a computer, but the spreadsheet by itself can achieve nothing without human agency framing the problems. There are a lot of places where human+computer could be vastly more useful now than they are, but are being overlooked in the rush to make computer-without-human systems.
and that they can be run on faster processors with larger data stores
Again, that’s also not clear. Human brains are probably not quantum computers, but they are highly connected neural networks. Neurons in the brain can connect to several thousand other neurons. Transistors on silicon chips can connect to single digits of other transistors. Simulating this with matrix multiplication is not space efficient and slows down as the connectivity grows (especially when you use back propagation to represent feed-backwards neural networks). Adding larger data stores increases latency.
So, your argument starts with three axioms, none of which is proven and at least one of which may not be true in the sort to medium term. Logical arguments that start from axioms that are not generally helpful.
extrapolating current trends, how much longer will humans be useful for anything at all?
Extrapolating from current trends, forever. That may not be good extrapolation because this kind of development often happens in bursts. Extrapolating from the difference engine, humans would be useful for menial calculation for a long time, but extrapolating from the first electronic computers gave a clear end point for that utility. AI systems running on quantum computers may be able to express forms of conscious intelligence that are so far beyond humans that they’re unrecognisable, given some clever bit of mathematics that no one has thought of yet.
I think that you’ve begged the setup. What is intelligence? Or, at least, what does it mean to compare intelligences? Is there a lattice of intelligence?
I always asked myself, ever since i got introduced to prolog at the early stages of my university module theoretical computer science and abstract datatypes - what would i use prolog for and why would i use it for that?
I know two use cases where prolog is used earnestly, both deprecated these days:
Gerrit Code Review allowed creating new criteria a change must fulfill before it can be submitted. Examples
SPARK, an Ada dialect, used prolog up to SPARK2005 (paper). Out of the formal verification annotations and the Ada code it created prolog facts and rules. With those, certain queries passed if (and only if) the requirements encoded in those annotations were satisfied. They since moved to third party SAT solvers, which allowed them to increase the subset of Ada that could be verified (at the cost of being probabilistic, given that SAT is NP-complete: a true statement might not be verified successfully, but a false statement never passes as true), so prolog is gone.
Datalog, which is essentially a restricted Prolog, has made a bit of a resurgence in program verification. There are some new engines like Soufflé designed specifically by/for that community. Not an example of Prolog per se, but related to your point 2.
A way I’ve been thinking about it is what if my database was more powerful & less boilerplate.
A big one for me is why can’t I extend a table with a view in the same way prolog can share the same name for a fact & a predicate/rule. Querying prolog doesn’t care about if what im querying comes from a fact (table) or a predicate (view).
This in practice i think would enable a lot of apps to move application logic into the database, I think this is a great thing.
move application logic into the database, I think this is a great thing
The industry as a whole disagrees with this vehemently. I’m not sure if you were around for the early days of RDBMS stored procedure hell, but there’s a reason they’re used fairly infrequently.
We actually do stored procedures at work & test them via rspec but it sucks. Versioning them also sucks to deal with. And the language is terrible from most perspectives, i think primarily it sucks going to a LSP-less experience.
I think to me though the root suckiness is trying to put a procedural language side by side a declarative one.
This wasn’t what I was saying with views.
I do think databases could be more debuggable & prolog helps here because you can actually debug your queries with breakpoints and everything. Wish i could do that with sql.
EDIT: but we continue to use stored procedures (and expand on them) because its just so much faster performance-wise than doing it in rails, and I don’t think any server language could compete with doing analysis right where the data lives.
Stored procedures can absolutely be the correct approach for performance critical things (network traversal is sometimes too much), but it also really depends. It’s harder to scale a database horizontally, and every stored procedure eats CPU cycles and RAM on your DB host.
I agree, prolog != SQL and can be really nice which may address many of the issues with traditional RDBMS stored procedures.
I do think databases could be more debuggable & prolog helps here because you can actually debug your queries with breakpoints and everything. Wish i could do that with sql.
Yeah. DBs typically have pretty horrible debugging experiences, sadly.
I feel that that this is a very US-coastal point of view, like one that is common at coastal start-ups and FAANG companies but not as common elsewhere. I agree with it for the most part, but I suspect there are lots of boring enterprise companies, hospitals, and universities, running SQL Server / mostly on Windows or Oracle stacks that use the stored procedure hell pattern. I would venture that most companies that have a job title called “DBA” use this to some extent. In any case I think it’s far from the industry as a whole
Nah, I started my career out at a teleco in the Midwest, this is not a SV-centric opinion, those companies just have shit practices. Stored procedures are fine in moderation and in the right place, but pushing more of your application into the DB is very widely considered an anti-pattern and has been for at least a decade.
To be clear, I’m not saying using stored procedures at all is bad, the issue is implementing stuff that’s really data-centric application logic in your database is not great. To be fair to GP, they were talking about addressing some of the things that make approaching thing that way suck
The industry as a whole disagrees with this vehemently. I’m not sure if you were around for the early days of RDBMS stored procedure hell, but there’s a reason they’re used fairly infrequently.
… in the same way prolog can share the same name for a fact & a predicate/rule. Querying prolog doesn’t care about if what im querying comes from a fact (table) or a predicate (view).
somewhat narrowly.
Sure we do not want stored procs, but
moving Query complexity to a database (whether it is an in-process-embedded database, or external database) is a good thing.
Queries should not be implemented manually using some form of a ‘fluent’ APIs written by hand. This is like writing assembler by hand, when optimizing compilers exists and work correctly.
These kinds of query-by-hand implementations within an app, often lack global optimization opportunities (for both query and data storage).
If these by-hand implementations do include global optimizations for space and time - then they are complex, and require maintenance by specialized engineers (and that increases overall engineering costs, and may make existing system more brittle than needed).
Also, we should be using in-process databases if the data is rather static, and does not need to be distributed to other processes (this is well served by embedding prolog)
Finally, prolog-based query also includes defining ‘fitment tests’ declaratively. Then prolog query responds finding existing data items that ‘fits’ the particular fitment tests. And that’s a very valuable type of query for applications that need to check for ‘existence’ of data satisfying a set of, often complex, criteria.
Databases can also be more difficult to scale horizontally. It can also be more expensive if you’re paying to license the database software (which is relatively common). I once had the brilliant idea to implement an API as an in-process extension to the DB we were using. It was elegant, but the performance was “meh” under load, and scaling was more difficult since the whole DB had to be distributed.
I have a slightly different question: does anybody use prolog for personal computing or scripts? I like learning languages which I can spin up to calculate something or do a 20 line script. Raku, J, and Frink are in this category for me, all as different kinds of “supercalculators”. Are there one-off things that are really easy in Prolog?
I’d say anything that solves “problems” like Sudoku or these logic puzzles I don’t know the name of “Amy lives in the red house, Peter lives next to Grace, Grace is amy’s grandma, the green house is on the left, who killed the mayor?” (OK, I made the last one up).
When I planned my wedding I briefly thought about writing some Prolog to give me a list of who should sit at which table (i.e. here’s a group of 3, a group of 5, a group of 7 and the table sizes are X,Y,Z), but in the end I did it with a piece of paper and bruteforcing by hand.
I think it would work well for class schedules, I remember one teacher at my high school had a huge whiteboard with magnets and rumour was he locked himself in for a week before each school year and crafted the schedules alone :P
The “classical” examples in my Prolog course at uni were mostly genealogy and word stems (this was in computer linguistics), but I’m not sure if that would still make sense 20y later (I had a feeling in this particular course they were a bit behind the time even in the early 00s).
I’d be interested to see a comparison like this. I don’t really know z3, but my impression is that you typically call it as a library from a more general-purpose language like Python. So I imagine you have to be aware of how there are two separate languages: z3 values are different than Python native values, and some operations like if/and/or are inappropriate to use on z3 values because they’re not fully overloadable. (Maybe similar to this style of query builder.)
By contrast, the CLP(Z) solver in Prolog feels very native. You can write some code thinking “this is a function on concrete numbers”, and use all the normal control-flow features like conditionals, or maplist. You’re thinking about numbers, not logic variables. But then it works seamlessly when you ask questions like “for which inputs is the output zero?”.
It’s really good for parsing thanks to backtracking. When you have configuration and need to check constraints on it, logic programming is the right tool. Much of classical AI is searching state spaces, and Prolog is truly excellent for that. Plus Prolog’s predicates are symmetric as opposed to functions, which are one way, so you can run them backwards to generate examples (though SMT solvers are probably a better choice for that today).
That subjectively resembles parser combinator libraries. I guess if you parse with a general-purpose language, even if the structure of your program resembles the structure of your sentences, you give up on getting anything for free; it’s impossible for a machine to say “why” an arbitrary program failed to give the result you wanted.
You can insert cuts to prevent backtracking past a certain point and keep a list of the longest successful parse to get some error information, but getting information about why the parse failed is hard.
I have used it to prototype solutions when writing code for things that don’t do a lot of I/O. I have a bunch of things and I want a bunch of other things but I’m unsure of how to go from one to the other.
In those situations it’s sometimes surprisingly easy to write the intermediary transformations in Prolog and once that works figure out “how it did it” so it can be implemented in another language.
Porting the solution to another language often takes multiple times longer than the initial Prolog implementation – so it is really powerful.
You could use it to define permissions. Imagine you have a web app with all kinds of rules like:
students can see their own grades in all courses
instructors and TAs can see all students’ grades in that course
people can’t grade each other in the same semester (or form grading cycles)
You can write down each rule once as a Prolog rule, and then query it in different ways:
What grades can Alice see?
Who can see Bob’s grade for course 123, Fall 2020?
Like a database, it will use a different execution strategy depending on the query. And also like a database, you can separately create indexes or provide hints, without changing the business logic.
For a real-world example, the Yarn package manager uses Tau Prolog–I think to let package authors define which version combinations are allowed.
When you have an appreciable level of strength with Prolog, you will find it to be a nice language for modeling problems and thinking about potential solutions. Because it lets you express ideas in a very high level, “I don’t really care how you make this happen but just do it” way, you can spend more of your time thinking about the nature of the model.
There are probably other systems that are even better at this (Alloy, for instance) but Prolog has the benefit of being extremely simple. Most of the difficulty with Prolog is in understanding this.
That hasn’t been my experience (I have written a non-trivial amount of Prolog, but not for a long time). Everything I’ve written in Prolog beyond toy examples has required me to understand how SLD derivation works and structure my code (often with red cuts) to ensure that SLD derivation reaches my goal.
This is part of the reason that Z3 is now my go-to tool for the kinds of problems where I used to use Prolog. It will use a bunch of heuristics to find a solution and has a tactics interface that lets my guide its exploration if that fails.
I don’t want to denigrate you, but in my experience, the appearance of red cuts indicates deeper problems with the model.
I’m really curious if you can point me to a largish Prolog codebase that doesn’t use red cuts. I always considered them unavoidable (which is why they’re usually introduced so early in teaching Prolog). Anything that needs a breadth-first traversal, which (in my somewhat limited experience) tends to be most things that aren’t simple data models, requires red cuts.
Unfortunately, I can’t point you to a largish Prolog codebase at all, let alone one that meets certain criteria. However, I would encourage you to follow up on this idea at https://swi-prolog.discourse.group/ since someone there may be able to present a more subtle and informed viewpoint than I can on this subject.
I will point out that the tutorial under discussion, The Power of Prolog, has almost nothing to say about cuts; searching, I only found any mention of red cuts on this page: https://www.metalevel.at/prolog/fun, where Markus is basically arguing against using them.
Because it lets you express ideas in a very high level, “I don’t really care how you make this happen but just do it” way, you can spend more of your time thinking about the nature of the model.
So when does this happen? I’ve tried to learn Prolog a few times and I guess I always managed to pick problems which Prolog’s solver sucks at solving. And figuring out how to trick Prolog’s backtracking into behaving like a better algorithm is beyond me. I think the last attempt involved some silly logic puzzle that was really easy to solve on paper; my Prolog solution took so long to run that I wrote and ran a bruteforce search over the input space in Python in the time, and gave up on the Prolog. I can’t find my code or remember what the puzzle was, annoyingly.
I am skeptical, generally, because in my view the set of search problems that are canonically solved with unguided backtracking is basically just the set of unsolved search problems. But I’d be very happy to see some satisfying examples of Prolog delivering on the “I don’t really care how you make this happen” thing.
How is that strange? It verifies that the bytecode in a function is safe to run and won’t underflow or overflow the stack or do other illegal things.
This was very important for the first use case of Java, namely untrusted applets downloaded and run in a browser. It’s still pretty advanced compared to the way JavaScript is loaded today.
I mean I can’t know from the description that it’s definitely wrong, but it sure sounds weird. Taking it away would obviously be bad, but that just moves the weirdness: why is it necessary? “Give the attacker a bunch of dangerous primitives and then check to make sure they don’t abuse them” seems like a bad idea to me. Sort of the opposite of “parse, don’t verify”.
Presumably JVMs as originally conceived verified the bytecode coming in and then blindly executed it with a VM in C or C++. Do they still work that way? I can see why the verifier would make sense in that world, although I’m still not convinced it’s a good design.
You can download a random class file from the internet and load it dynamically and have it linked together with your existing code. You somehow have to make sure it is actually type safe, and there are also in-method requirements that have to be followed (that also be type safe, plus you can’t just do pop pop pop on an empty stack). It is definitely a good design because if you prove it beforehand, then you don’t have to add runtime checks for these things.
And, depending on what you mean by “do they still work that way”, yeah, there is still byte code verification on class load, though it may be disabled for some part of the standard library by default in an upcoming release, from what I heard. You can also manually disable it if you want, but it is not recommended. But the most often ran code will execute as native machine code, so there the JIT compiler is responsible for outputting correct code.
As for the prolog part, I was wrong, it is only used in the specification, not for the actual implementation.
You can download a random class file from the internet and load it dynamically and have it linked together with your existing code. You somehow have to make sure it is actually type safe, and there are also in-method requirements that have to be followed (that also be type safe, plus you can’t just do pop pop pop on an empty stack). It is definitely a good design because if you prove it beforehand, then you don’t have to add runtime checks for these things.
I think the design problem lies in the requirements you’re taking for granted. I’m not suggesting that just yeeting some untrusted IR into memory and executing it blindly would be a good idea. Rather I think that if that’s a thing you could do, you probably weren’t going to build a secure system. For example, why are we linking code from different trust domains?
Checking untrusted bytecode to see if it has anything nasty in it has the same vibe as checking form inputs to see if they have SQL injection attacks in them. This vibe, to be precise.
…Reading this reply back I feel like I’ve made it sound like a bigger deal than it is. I wouldn’t assume a thing was inherently terrible just because it had a bytecode verifier. I just think it’s a small sign that something may be wrong.
Honestly, I can’t really think of a different way, especially regarding type checking across boundaries. You have a square-shaped hole and you want to be able to plug there squares, but you may have gotten them from any place. There is no going around checking if random thing fits a square, parsing doesn’t apply here.
Also, plain Java byte code can’t do any harm, besides crashing itself, so it is not really the case you point at — a memory-safe JVM interpreter will be memory-safe. The security issue comes from all the capabilities that JVM code can access. If anything, this type checking across boundaries is important to allow interoperability of code, and it is a thoroughly under-appreciated part of the JVM I would say: there is not many platforms that allow linking together binaries type-safely and backwards compatibly (you can extend one and it will still work fine).
Honestly, I can’t really think of a different way, especially regarding type checking across boundaries. You have a square-shaped hole and you want to be able to plug there squares, but you may have gotten them from any place. There is no going around checking if random thing fits a square, parsing doesn’t apply here.
Also, plain Java byte code can’t do any harm, besides crashing itself, so it is not really the case you point at — a memory-safe JVM interpreter will be memory-safe. The security issue comes from all the capabilities that JVM code can access. If anything, this type checking across boundaries is important to allow interoperability of code, and it is a thoroughly under-appreciated part of the JVM I would say: there is not many platforms that allow linking together binaries type-safely and backwards compatibly (you can extend one and it will still work fine).
Well, how is this different from downloading and running JS? In both cases it’s untrusted code and you put measures in place to keep it from doing unsafe things. The JS parser checks for syntax errors; the JVM verifier checks for bytecode errors.
JVMs never “blindly executed” downloaded code. That’s what SecurityManagers are for. The verifier is to ensure the bytecode doesn’t break the interpreter; the security manager prevents the code from calling unsafe APIs. (Dang, I think SecurityManager might be the wrong name. It’s been soooo long since I worked on Apple’s JVM.)
I know there have been plenty of exploits from SecurityManager bugs; I don’t remember any being caused by the bytecode verifier, which is a pretty simple/straightforward theorem prover.
In my experience, it happens when I have built up enough infrastructure around the model that I can express myself declaratively rather than procedurally. Jumping to solving the problem tends to lead to frustration; it’s better to think about different ways of representing the problem and what sorts of queries are enabled or frustrated by those approaches for a while.
Let me stress that I think of it as a tool for thinking about a problem rather than for solving a problem. Once you have a concrete idea of how to solve a problem in mind—and if you are trying to trick it into being more efficient, you are already there—it is usually more convenient to express that in another language. It’s not a tool I use daily. I don’t have brand new problems every day, unfortunately.
Some logic puzzles lend themselves to pure Prolog, but many benefit from CLP or CHR. With logic puzzles specifically, it’s good to look at some example solutions to get the spirit of how to solve them with Prolog. Knowing what to model and what to omit is a bit of an art there. I don’t usually find the best solutions to these things on my own. Also, it takes some time to find the right balance of declarative and procedural thinking when using Prolog.
Separately, being frustrated at Prolog for being weird and gassy was part of the learning experience for me. I suppose there may have been a time and place when learning it was easier than the alternatives. But it is definitely easier to learn Python or any number of modern procedural languages, and the benefit seems to be greater due to wider applicability. I am glad I know Prolog and I am happy to see people learning it. But it’s not the best tool for any job today really—but an interesting and poorly-understood tool nonetheless.
I have an unexplored idea somewhere of using it to drive the logic engine behind an always on “terraform like” controller.
Instead of defining only the state you want, it allows you to define “what actions to do to get there”, rules of what is not allowed as intermediary or final states and even ordering.
Datalog is used for querying some databases (datomic, logica, xtdb). I think the main advantages claimed over SQL are that its simple to learn and write, composable, and some claims about more efficient joins which I’m skeptical about.
Attestation means you can only use approved clients, which is terrible for competition and innovation (sorry, it’s now impossible to make a new browser or OS!)
Sounds really bad. This will make it hard to run non-mainstream platforms.
I guess regulators might step in and demand alternative modes of attestation, like they have done in case of iOS and the single-store monopoly. However, they are exceedingly slow at doing so. For instance, now it is impossible to do online banking in some places if you don’t run iOS or Android. Something as innocent as AOSP is not supported, even if you run the same banking app, due to the lack of SafetyNet attestation.
It’s also not clear to me that policymakers have any particular reason to care about non-commercial platforms or software modification as civil liberties issues. So we might not get the regulation we want…
Honestly not a bad time to start thinking about what the rules OUGHT to be in an ideal world. Even if we can’t get there anytime soon, knowing where we want to go has to help somehow.
The EU has a good reason to care. All of the big OS vendors are based in the US. If things require an attestation that only a US company can provide then this makes it impossible for any EU startup to ever grow to being a big company in this space.
This is especially true when you consider that things like the YouTube and Android are owned by the same US entity. If Google decides to require attestation to watch YouTube videos (so that they know that you aren’t using a client that skips ads, for example) then there is a fairly clear argument under existing monopoly law that they’re using their effective monopoly in one market to ensure that there can be no competition entering another market where they’re a significant player.
I think we need to learn a lot from the problems with DRM here. We pushed back on the technologies, rather than the uses. We didn’t block the technology in standards bodies (in part because there are some non-evil uses, such as access control within an organisation) and we didn’t get regulations on acceptable use. I’d love to see using DRM that prevents users from exercising fair use rights treated as vigilanteism and grounds for having copyright on the work in question revoked. Similarly, anyone using this kind of attestation to lock in clients to a particular platform should be subject to serious antitrust investigation.
The political leaders of the EU have a good reason to care that European keys find their ways into the TPMs of digital devices. They have no reason whatsoever to care about civil liberties of Europeans, or that people can run their own libre software on their devices. Quite the contrary - free computing is a threat to governing bodies, especially those that like to grow in size and power. The TPM menace will only grow worse as time goes on.
My immediate vision is of a future where I end up having to literally drive to the bank to pay my bills because, eventually, I will no longer run a rights-infringing OS that happens to be the only one supported by online banking. It doesn’t even seem farfetched. I already am excluded from lots of software, games, and online services that require an OS I refuse to utilize, and the rate of that exclusion definitely seems to be accelerating quickly.
Mutable state is not “evil”.^ Shared mutable state is not “evil”. Yes, undisciplined use of either makes software harder to reason about. But there is nothing intrinsically “evil” about shared mutable state. It’s a fundamental component of the machine model that underlies our computers.
^ It’s meaningless to use terms like “evil” w.r.t. technology.
Fair point. I wasn’t clear at all why the link is interesting. It talks about program correctness (which is a good part of the linked article) from a FP/IP perspective. Hillel’s article also talks about blanket statemens in the vein of the parent comment.
EDIT: Hillel’s article is about the issue you mentioned in your other comment in this thread, if it’s easier to prove programs correct in IP or FP.
I’m not too familiar with formal verification (aside from TLA+ style); is there a reason imperative code is easier to prove correct? Is it primarily due to the tooling, or innate to the math backing formal verification?
Mainly asking because I was under the impression that functional languages stick far more closely to CS math, while imperative is less so.
For static analysis, I have to say I’m confused here. Strong type systems (a feature of many functional languages, but not necessarily) and pure functions seem like they would lend themselves far more easily to static analysis.
There is a large gap in effort invested in static analysis tooling for imperative vs. functional programming; for a while people basically focused on just analyzing C code, and it shows (without saying much about the fundamental difficulty). (For example, SMT solvers became relatively good at numerical reasoning, and generally disappointing at reasoning on rich datatypes, but this is not because integer manipulations are easier, it is because early they focused on programs doing a lot of array indexing.)
My experience is that functional code in most cases has simpler invariants and specifications.
Most static analysis tools on imperative programs are meant to prove safety properties, typically the absence of undefined behaviors, or some relatively safe asserts. If we are talking about “proving correct”, we are talking full correctness. And there the state of the art seems much stronger for functional programs. Do we have any example of notable program with a full correctness proof, written from the start in an imperative style? Probably the two flagship examples of full verified programs are CompCert (a C compiler) and seL4 (a microkernel), CompCert is written in a very functional mix of Coq and OCaml, and seL4 is a Haskell program that is refined into a C implementation. I know of a few cases of verified programs that were written in an imperative style first, mostly in the crypto domain, because it was a design requirement to generate C code from the start (the HACL* stuff0.
(This point suffers from a dual of the bias argument of point (1): one could argue that most large verified programs are written in a functional style because most program-verification practitioners prefer functional programming. I don’t think this suffices to explain the gap, but it is of course worth keeping in mind.)
If we are talking about “proving correct”, we are talking full correctness. And there the state of the art seems much stronger for functional programs.
FP languages are overrated when it comes to proving full correctness. seL4 and CompCert were written at a pace of 2 LoC/person-day, which is utterly outclassed by IronFleet. That was done in the imperative Dafny and written at the blistering pace of 4 LoC/person-day.
Total correctness is just a really hard problem regardless of the paradigm you use.
(I’ve heard SPARK people claim they can do better than 4 loc/day, but I haven’t analyzed a large SPARK project yet.)
I’m not familiar with the IronFleet work, but here is section 6.2 of the “IronFleet: Proving Practical Distributed Systems Correct” paper (Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch,
Bryan Parno, Michael L. Roberts, Srinath Setty, Brian Zill; 2015):
Verifying imperative code is challenging compared with
verifying purely functional code, even when using a state-
of-the-art tool like Dafny that is designed for imperative
programs (§2.2). Thus, we found it profitable to implement
the system in two stages. First, we develop an implementation
using immutable value (functional) types and show that it
refines the protocol layer. Avoiding heap reasoning simplifies
the refinement proof, but, it produces a slow implementation,
since it cannot exploit the performance of heap references.
In the second stage, we replace the value types with mutable
heap types, improving performance while solving only a
narrow verification problem.
We apply this pattern in building IronRSL and IronKV;
e.g., the functional implementation manipulates IP addresses
as value types and the performant one uses references to OS
handles. This strategy takes advantage of Dafny’s support for
mixing functional programming and imperative programming
styles: we can first run the functional code and measure its
performance, then optimize the performance-critical sections
into imperative heap-based code as needed. Using a language
without good functional programming support (such as C)
would have made it harder to pursue this strategy.
It looks like the IronFleet authors agree with what I said above, and their verification approach is close, when it comes to implementation, to the one of SeL4: implement a functional program, then refine into an imperative program.
(One could make a qualitative distinction on whether the functional program merely serves as a model – as automata-style state models or is a “real implementation”, and I don’t know the status here.)
I don’t have any open code to share, but some exceptions come from control and real-time systems I have worked in. Verifying state machines, which are a natural way to represent some control problems, and/or proving they satisfy time constraints, is sometimes easier with imperative code.
In general, I agree functional code is easier to prove correct thanks to referential transparency. I just stated there are some exceptions.
If you’re interested in any way in learning about proofs and formal verification, I can’t recommend Isabelle enough. I never proved anything in my life before using Isabelle, and now I’m able to do relatively non-trivial things in it.
I think it’s easier than all of the other proof assistants to get into, because the logic (HOL) is simpler, and is pretty much like ML / Haskell with a few additional concepts. The automation is also really good, and for a while you can get away with proving things with a one liner: by auto, without understanding too much of what’s going on under the hood.
I think that’s really important, because otherwise it’s really hard to achieve liftoff when you don’t know how to specify nor prove things. Proof automation allows you to focus a lot more on the specification side first, and then you can build on getting better at the actual act of proving over time.
How does Isabelle intersect with formal verification generally? I think I remember reading it’s used to prove things about the output assembly code or something?
The flagship example is the seL4 OS. They have a C parser which connects to a formal C semantics in Isabelle, so they verify actual C code against a functional correctness specification.
Then, and this is my personal favorite project, there’s also Cogent which is a language that compiles to C, but it uses the pattern of certifying compilation to produce a proof of correctness along with it. They’ve used this to implement verified file systems.
It was also used to verify several properties about WebAssembly, where the formalization found soundness errors in the type system that led to changes to the spec IIRC.
It also supports extraction, similar to Coq, where you can extract verified components to Haskell / OCaml, etc. I think the wasm project used this to extract a reference interpreter for testing.
The proofs for seL4 go even deeper (for Armv7): the seL4 team did binary verification, where they verified that the compiled object code corresponds to the C code that should have been compiled, eliminating the compiler from the trusted code base.
(though this isn’t done in Isabelle, they used SMT-techniques instead)
Coq has more users, there’s no getting around that. I assuming you know about Concrete Semantics, though that’s not really about large-scale verification. I’ve gotten a lot of information by reading seL4 papers about that.
Other than that, I use Isabelle to do exercises for any book. For example, I did it for Types and Programming Languages, and that was a great experience. The same should apply to FRAP and Software Foundations - they do have some Coq-specific content, but everything there can be formalized in Isabelle.
I think there’s a relative void for what you’re asking, for sure. Proof engineering is still very niche, and the already-small community is still fragmented.
I think this is slightly misleading. BEAM saves them the money and they like the affordances in Elixir. I was pretty surprised until I saw that their baseline was Ruby. BEAM is a lot slower than most low-level languages, but Ruby is well known to be painfully slow. Last time I looked at the language shootout game results, it was a quarte of the speed of Squeak (Smalltalk). Squeak is written to be flexible and understandable at the expense of performance, Ruby eliminates the features of Smalltalk that add the worse performance overhead and still manages to be slow.
I’m not sure it’s only speed. Just by having cheaper parallelism (and ‘hanging’ connections) you can do a lot with the BEAM where a multi-threaded (or multi-proc) server in ruby would need a lot more memory (and probably CPU).
That’s true. I first used Erlang during my PhD and wrote code that ran on my single-core PowerBook and scaled linearly to the 64-processor (MIPS) SGI box that I deployed it on. I have never done that in any other language. Unfortunately, per core it ran at 1/10th the speed of the C version. I definitely couldn’t do it in a Smalltalk-family language like Ruby without some very rigid discipline that would remove most of the value such a language.
It would be interesting to look at a baseline like Pony, which is much faster for straight-line execution than BEAM.
It compounds too. A lot of things become easier like a long running pool of connections to your db, which makes the caching on postgres far more efficient as an example.
Cost of crashes are lower too, latency tend to handle high load better, etc etc. It compounds pretty fast into really tangible results.
I briefly tried NixOS. I love the idea, and having my configuration (which I try to keep simple) available right there is very nice. Unfortunately I hit a couple snags:
No British dictionary available by default for Aspell. Didn’t know how to import it, had to make do with the US one.
Perl (sloccount) nagged me about my locales not being set up properly, and I failed to please it.
GNU make (I think it was GNU make?) seemed to behave strangely when I tried the ?= assignment. Not sure if this is me not understanding environment variables, some Nix quirk, or the particular make flavour I was using.
Clang sanitizers crashed on me, with an error message clearly saying it’s not my code’s fault.
I’m sure these could be fixed, perhaps even easily so. If I was more serious about Nix I would probably have pushed through, solved these, and contributed. I like Nix, and maybe I’ll come back some day. Right now unfortunately I have other priorities, so I went back to Ubuntu.
That said, I’m not ruling out revising Nix in a few years.
I had much the same experience! That was almost 4 years ago now, though, and this time around it’s clicked.
I think the main thing Nix gives me despite having to work around things like these is that the workarounds are (in their own way, at least) permanent. Once you get the config into a given state, it’s a done deal, and this is super valuable to me as someone who uses a number of different “personal” machines in different contexts. I find myself putting more time into the refinement of my (human interface) systems because it’s not just sitting in a dotfile, or a git-backed dotfile, or a (…), but something structured and expressive enough to do ~anything. (like with patching fish(1) in this post.)
Adding the time dimension to system configuration in a legible way means you are building something, not just tweaking nobs, and though I didn’t think I’d ever appreciate the need, having implemented it, I’m very content.
Nix is a whole new paradigm, so there’s a lot of stuff to get used to to be idiomatic. Unfortunately the documentation sucks, and the maintainers seem to disagree that it sucks, saying that it’s irreducible complexity (bull because Nix derivations are incredibly simple compared to other packaging systems when written idiomatically) or that people just have to get used to it (bull because it’s really effing hard to discover things when they are not hyperlinked together, or the tooling produces alien output).
and the maintainers seem to disagree that it sucks
…or not.
Shame. One thing’s for sure, I probably won’t come back until documentation gets better. Not just the general stuff (which to be honest looked pretty good), but the boring stuff like how to discover the existence of a particular helper function, whose apparent absence were a reason for my departure. Or the complete description of the relevant options for any particular package I try to include in my configuration. I can’t be expected to look at the source package, I haven’t even stumbled upon how to find and read it.
While we’re at it, one more thing that caused me to leave: using ?= assignment in make. I did to assign standard variables like CC and CFLAGS because users are supposed to be able to override this with environment variables, and, as far as I could tell, it’s also a convention to tell users “go ahead, you can override this safely”. When I used the regular = assignment, one user asked me if it was safe to change the compiler, they genuinely weren’t quite sure (and they understandably wouldn’t take chances with a crypto library).
Problem is, stupid GNU Make ignores my default, even when the users don’t have their CC or CFLAGS environment variables set. Why? Because there’s a build-in default, that an explicit default does not override (because it’s “already set”). So instead of my specified default (gcc -std=c99), we get just cc… well, that’s what the GNU documentation says, but in reality I got c99.
I got really confused to be honest: why was Make truncating my option? Does it ignores whatever is between ?= and = or something? And of course my system didn’t have the c99 compiler, so I just gave up on the ?= idea, thinking maybe it was a BSD thing…
…until I retried it on my fresh Ubuntu system. And what do you know, it worked! Well, not quite, GNU Make was as stupid as ever, and still used c99 by default despite me specifying another default. Same deal for CFLAGS. But this time, my system had an alias, which lead me to understand that really, this stupidity from GNU Make was intentional.
Couldn’t have learned that from NixOS, though: it didn’t have that alias, so when I tried it there, I just thought there was “something special” going on that were confusing me, and just gave up on ?= for the time being.
Which reminded me, NixOS doesn’t have a /bin/env either. In so many places I see that we should prefer #! /bin/env sh and #! /bin/env python3 over #! /bin/sh or #! /usr/bin/python3. But that didn’t work with NixOS, so I ended up adding a hard link to the actual env program (maybe configuration could have done that for me).
I got a similar problem with pkg-config: there is some setup to do before I can just sudo make install a pkg-config aware tarball and expect pkg-config --cflags my_tarball to work. Out of the box it doesn’t. Again, I made it work the ugly way, not quite knowing what the proper way was. (Though I suspect the proper way is to never just type sudo make install in the first place, but instead write a Nix package for this source code, which I didn’t know how to do.)
All this to say, the GNU/Linux ecosystem has a lot assumptions baked in. Many of them are hard to guess, until we stumble upon a system, like NixOS, that breaks them. And boy does NixOS breaks a lot of such assumptions. So we need to either fix those breaks, or do things the Nix way even though the very software it packages does not play the same game. There’s a rather tall wall to climb, and I don’t know how.
This thing about maintainers allegedly thinking their documentation is fine? It’s worrying. Long term, it could even kill Nix and NixOS. I really hope it gets better.
Yeah, that one was my mistake (for just one script, all the others use /usr/bin/env, that went unnoticed because Ubuntu (my previous system) actually conflates /bin and /usr/bin.
Now it’s all corrected and harmonised into one of the following:
#! /bin/sh
#! /usr/bin/env python3
(Hopefully my shell scripts stick to the old Bourne shell, without any Bash extension.)
GNU (and I think BSD) env‘s “canonical” home is /usr/bin, but lots of distros merged /usr/bin and /bin a long time ago which has caused various hardcoded paths to seep from one into the other. env has always lived in /usr/bin, as far as I know, or in any case it’s been there for as long as I remember it; but it “feels” like something that ought to be in /bin, and /bin/env just happens to work because /bin is now a symlink to /usr/bin almost everywhere.
I installed NixOS on my work laptop during the early stages of the pandemic, when I should probably have been doing something else but didn’t have any sanity left to do those things. Before that I had bounced off it a couple of times, much in the manner you describe. For what it’s worth the amount of snags that need figuring out seem to be bounded and they grow at a rate measured in years. So there is a hump to get over at first, but if you get over it the sailing is very smooth after that.
I agree that environment.systemPackages = [(pkgs.aspellWithDicts (dicts: [dicts.en]))] is nicer than environment.systemPackages = [pkgs.aspell pkgs.aspellDicts.en], but you seem to be saying that it gives a different result? If so, how?
If you install them separately, aspell doesn’t know the dictionaries are available since they’re completely separate paths. aspellWithDicts generates the correct merge/wrapper to bind them together. This is a usual problem with apps that require plugins.
Only English dictionary I got from this one was US. I guess it’s an “oh but of course you’re using the old method” or something, but it’s the method I found, and searching failed to turn up the other one. Also, had I tried it blind, I would have imitated Python, and maybe come up with something like the following at best:
(aspell.withDicts (dicts: [dicts.fr, dicts.en]))
I mean, the aspellWithDicts package would have been a total unknown for me.
This is something that requires a bit of readjustment to Nix and its way of doing things, as it does not rely on dynamic linking or uncontrolled environment variables.
All tools are composed by indicating subpackages with the appropriate helper function. There are helper functions for everything ranging from TeX to Emacs.
That’s less a Nix thing than a nixpkgs-specific thing. The discoverability of those helpers is awful. For example, if you just search aspell on search.nixos.org/packages, you just get aspell and aspellDicts.*. There’s no indication that the aspell package includes a helper function for adding dictionaries.
I agree. The problem right now is that Nix has no clear learning path. Even if you are willing to put a lot of effort, documentation is patchy and you end up needing to look at source. The split between flakes and channels makes this even more difficult. Guix is much more coherent.
I love both Haskell and OCaml, and I have used them quite extensively.
My feel is that OCaml is on an upward trend. It is in the process of addressing, or has already addressed, some major pain points: multicore and better control of impurity (via effects). Plus, ML in general is gaining exposure with Rust, Swift and Scala. Interesting libraries are getting written, and there are lots of OCaml users in the formal methods community.
Haskell, on the other hand, seems to be declining. Some community leaders have moved elsewhere. The standard has become stagnant and the library ecosystem does not look very lively. There is no real effort to streamline the whole Haskell stack for industrial users, perhaps because the language wants to optimize for research.
It seems like Jane St is funding almost all non-academic OCaml compiler and runtime work?
That makes all the difference in the world … Getting like 5 really good people full time, is 1000x better than getting 100 people in their spare time (usually researchers)
e.g. JavaScript is a funded language because it’s attached to certain businesses, and I think the same is true of OCaml. Not saying that’s good or bad, but it appears to be the truth.
Also Tarides (supported by Tezos) and, of course, INRIA are doing real-world OCaml development, e.g. multicore.
I agree with you, having some full-time core developers makes a huge difference. I think it is a shame many big Haskell users are not giving a bit more back by funding such a core.
I mean, Haskell and Haskell tooling are generally so good that I’m often more annoyed than excited by new release (because if they changed anything there’s a small chance it got worse. Would be hard for it to get better…)
The Functional Approach to Programming with Caml by Guy Cousineau and Michel Mauny is really good.
However, it is not an OCaml reference, but rather a functional programming textbook that overlaps with TAPL and other textbooks. It is a bit of Caml + PLT.
It’s not really simpler, just slightly different. Not lazy, not pure, and object oriented. It’s the inspiration for a whole family of ocaml clones like swift, Scala, rust, etc
Sure, I know, I have programmed quite a lot in OCaml and SML.
Haskell was heavily influenced by Miranda, which was a lazy successor to ML, and also by SML. So they are all pretty close in the lineage tree of programming languages.
My question was a bit more practical, about the niche both are trying to fill, and actual usage.
It has much fewer possibilities for writing code that people who are not fluent in the language don’t understand, because it’s much more “wordy”, like other functional languages and less “what does this overloaded operator in this code-golfed line mean”?
not positive those three calamities were the only ones…
if there were funding and employment structures (e.g., cooperatives, unions, credit unions) that allowed community choice and control in a way that GPL allows for software… maybe there’d be options besides the company making police sticks.
Very happy to see cooperatives mentioned; I think that’s got to become a huge part of the FOSS ecosystem if we want to see FOSS economically stabilized. Currently working on a project for this and I hope it’ll be out in a few months.
Roughly speaking, if you want a FOSS project to grow beyond a one-person hobby project, then there are two paths typically acknowledged. One is to rely on donations; the other is to become a startup. Both have flaws. One rarely raises enough in donations to support flourishing software development. And becoming a startup often leads to investor pressure to go down the path of “open-core”, or “source-available” relicensing, or (if you had contributors sign a CLA) folding and going totally proprietary.
As an alternative, I think if FOSS developers formed worker cooperatives to support their projects, then they’d get more economic support than from donations, but without the negative investor pressure that comes from conventional VC-backed incorporation. But currently there’s not much help on how to form a cooperative, or manage it, nor really is there widespread understanding of what a cooperative is. To really help the FOSS movement, there should be an ecosystem of institutions to helping developers establish coops, manage them, and promote this course of action in the wider community. I’m trying to build a piece of this ecosystem right now.
It’s sometimes easy to forget that all of the software that we use is built and maintained by individuals. Even tools that feel like they’ve been around for ages. (Relevant XKCD: https://xkcd.com/2347/)
Does anyone know what this means for the project and community? Are other people able to take over management or was it a one man show? I remember an argument for neovim being that it was community driven whereas vim had a BDFL.
Christian is a long time contributor (and co-maintainer) of Vim and has commit access to the GitHub repo. It looks like he will step up as lead maintainer.
It has been a very long time since Bram was the sole developer on Vim, many of the changes are contributed by the community (with some notable exceptions). Bram would always commit the patches, but I would be very surprised if Bram’s passing significantly impacts the project.
I’m glad that people have access and can continue the work. Very sad that Christian didn’t get a chance to meet him in person though. You never know how much time you have with people.
Right now the EU is slowly starting to acknowledge this problem and pours a bit of cash into critical projects that are underfunded / maintained by a few.
Interestingly, a foundation called NLnet has an important role in selecting projects that get funded. AFAIK, Bram was an employee of NLnet.
This does make me regret selling my M1 Mini. Apple pissed me off enough with the whole CSAM/on device scanning thing (along with a range of other things) that I got rid of it, at some substantial loss, figuring that the Linux projects on it wouldn’t come to anything useful (at the time, they were still working out some basic functionality). Asahi has come a long ways since then.
They’ve done a really, really good job with hardware reverse engineering, and have quite exceeded my expectations for what they’d accomplish - I’m glad to see it!
I’m curious as to why you regret selling the hardware. A company proposes awful spyware for it’s hardware which you respond by deciding to sell it’s product but now you experience regret because you can’t test out software that the same company is not supporting or encouraging in the slightest? What is it about Asahi that makes you want an Apple device? I know Apple makes good hardware but I don’t think the hardware is THAT good that some independently contributed software is a game changer for it. Especially when many other vendors make pretty great hardware that support the software.
I like ARM chips, and I utterly love what Apple has done with the SoC design - huge caches, and insane gobs of memory bandwidth. The performance out of it backs the theory I’ve run with for a while that a modern CPU is simply memory limited - they spend a lot of their time waiting on data. Apple’s designs prove this out. They have staggeringly huge L1 cache for the latency, and untouchable memory bandwidth, with the performance one expects of that. On very, very little power.
Various people have observed that I like broken computers, and I really can’t argue. I enjoy somewhat challenging configurations to run - Asahi on Apple hardware tickles all those things, but with hardware that’s actually fast. I’ve used a variety of ARM SBCs as desktops for years now - Pis, ODroids, I had a Jetson Nano for a while, etc. They’re all broken in unique and novel ways, which is interesting, and a fun challenge to work around. I just didn’t expect Asahi to get this usable, this quickly.
I sold the M1 Mini and a LG 5k monitor at about a $1000 loss over what I’d paid for them (over a very short timescale - I normally buy computers and run them to EOL in whatever form that takes). I didn’t have any other systems that could drive the 5k, so it made sense to sell both and put a lower resolution monitor in the spot, but the M1/LG was still the nicest computer I’ve ever used in terms of performance, responsiveness, etc. And it would, in Rosetta emulation, run Kerbal Space Program, which was about the one graphically demanding thing I used to do with computers.
In any case, getting rid of it drove some re-evaluation of my needs/desires/security stances, and now I run Qubes on just about everything, on x86. Painful as it is to say, relative to my previous configurations, this all qualifies as “Just works.”
What did you replace it with? The basic Mac Mini M2 is really cheap now at ~$600. I run NixOS on a decade-old NUC, and it is tempting as a replacement. A good fanless x86 is easily 50% more and not nearly as energy efficient as the Mini.
However, right now one needs to keep macOS to do firmware updates. And AFAIK there is limited video output support on the M2.
An ASRock 4x4 Box 5000U system, with a 5800U and 64GB RAM. It dual boots QubesOS and Ubuntu, though almost never runs Ubuntu, and the integrated graphics aren’t particularly good (the theory had been that I could do a touch of light gaming in Ubuntu, but reality is that it doesn’t run anything graphically intensive very well). It was not a well thought out purchase, all things considered, for my needs. Though, at the time, I was busily re-evaluating my needs and assumed I needed more CPU and RAM than I really do.
I’m debating stuffing an ODroid H3+ in place of it. It’s a quad core Atom x86 small board computer of the “gutless wonder” variety, and it runs Qubes quite well, just with less performance than the AMD box. However, as I’ve found out in the migration to QubesOS, the amount of computer I actually need for my various uses is a lot less than I’ve historically needed, and a lot less than I assumed I would need when I switched this stuff out. It turns out, the only very intensive things I do anymore are some bulk offline video transcoding, and I have a pile of BOINC compute rigs I can use for that sort of task.
I pretty much run Thunderbird, a few Firefox windows, sometimes Spotify or PlexAmp (which, nicely, run on x86 - that was a problem in my ARM era), a few communications clients, and some terminals. If I have dev projects, I spin up a new AppVM or standalone VM to run them in, and… otherwise, my computers just spend more and more time shut down.
the same company is not supporting or encouraging in the slightest
That’s not quite true — apple went out of their way to make the boot secure for third-party OSs as well, according to one of the Asahi devs. So I don’t see them doing any worse than.. basically any other hardware company - those just use hardware components that already have a driver reverse engineered, or in certain cases contributed to some by the producing company, e.g. intel. Besides not having much incentive for opening up the hardware, companies often legally can’t do it due to patents not owned by them, only licensed.
And as for the laptop space, I would argue that the M-series is that good — no other device currently on the market get even in the same ballpark of their performance-efficiency plot to the point I can barely use my non-M laptop as a mobile device.
This is the attitude that I don’t understand. To pick four big chip-makers, I would rank Apple below nVidia, Intel, and AMD; the latter three all have taken explicit steps to ensure that GNU/Linux cleanly boots with basic drivers on their development and production boards. Apple is the odd one out.
On my m1 mac laptop I can work a full 10 hour work day compiling mutliple times without once plugging in my machines. The compiles are significantly faster than other machines and the laptop barely get’s above room temperature.
This is significantly better hardware wise than any other machine I could buy or build on the market right now. It’s not even a competition. Apples hardware is so far ahead of the competition right now that it looks like everyone else is asleep at the wheel.
If you can run your favorite OS on it and get the same benefits why wouldn’t you?
My most recent laptop purchase was around $50 USD. My main workstation is a refurbished model which cost around $150. My Android phone cost $200. For most of my life, Apple products have been firmly out of budget.
They had to, as servers are predominantly running linux and they are in the business of selling hardware components. Apple is not, so frankly I don’t even get the comparison.
Also, look back a bit earlier and their images are far from stellar, with plenty painstaking reverse engineering done by the Linux community. Also, nvidia is not regarded as a good linux citizen by most people, remember Linus’s middle finger? There has only recently been changes so their video cards could be actually utilized by the kernel through the modern display buffer APIs, instead of having to install a binary blob inside xserver coming with their proprietary driver.
The performance and fanless arguments are icing on the cake and completely moot to me. No previous CPU was ever hindering effectiveness of computing. While I’m glad a bunch of hardware fanatics are impressed by it, the actual end result of what the premium locked down price tag provides is little better in real workload execution. Furthermore they’re not sharing their advancements with greater computing world, they’re hoarding it for themselves. All of which is a big whoop-dee-doo if you’re not entranced by Apple’s first-world computing speeds mindset.
AMD definitely does; their biggest contribution is amd64. Even nVidia contributes a fair amount of high-level research back to the community in the form of GPU gems.
AMD definitely does; their biggest contribution is amd64
Which AMD covered in a huge pile of patents. They have cross licensing agreements with Intel and Via (Centaur) that let them have access to the patents, but anyone else who tries to implement x86-64 will hear from AMD’s lawyers. Hardly sharing with the world. The patents have mostly expired on the core bits of x86-64 now, but AMD protects their new ISA extensions.
Didn’t they back off from this at least though? It almost seemed like a semi rogue VP pushed the idea, which was subsequently nixed by likely Tim Cook himself. The emails leaked during that debacle point to a section of the org going off on it’s own.
They did. Eventually. After a year of no communications on the matter beyond “Well, we haven’t shipped it yet.”
I didn’t pay attention to the leaked emails, but it seemed an odd hill to die on for Apple after their “What’s on your phone is your business, not ours, and we’re not going to help the feds with what’s on your device” stance for so long. They went rather out of their way to help make the hardware hard to attack even with full physical access.
Their internal politics are their problem, but when the concept is released as a “This is a fully formed thing we are doing, deal with it,” complete with the cover fire about getting it done over the “screeching voices of the minority” (doing the standard “If you’re not with us, you’re obviously a pedophile!” implications), I had problems with it. Followed by the FAQ and follow on documents that read as though they were the result of a team running on about 3 days of no sleep, frantically trying to respond to the very valid objections raised. And then… crickets for a year.
I actually removed all Apple hardware from my life in response. I had a 2015 MBP that got deprecated, and a 2020 SE that I stopped using in favor of a flip phone (AT&T Flip IV). I ran that for about a year, and discovered, the hard way, that a modern flip phone just is a pile of trash that can’t keep up with modern use. It wouldn’t handle more than a few hundred text messages (total) on the device before crawling, so I had to constantly prune text threads and hope that I didn’t get a lot of volume quickly. The keypad started double and triple pressing after a year, which makes T9 texting very, very difficult. And for reasons I couldn’t work out nor troubleshoot, it stopped bothering to alert me of incoming messages, calls, etc. I’d open it, and it would proceed to chime about the messages that had come in over the past hour or two, and, oh yeah, a missed phone call. But it wouldn’t actually notify me of those when they happened. Kind of a problem for a single function device.
Around iOS 16 coming out, I decided that Lockdown mode was, in fact, what I was looking for in a device, so I switched back to my iOS device, enabled Lockdown, stripped the hell out of everything on it (I have very few apps installed, and nothing on my home screen except a bottom row of Phone, Messages, Element (Matrix client), and Camera), and just use it for personal communications and not much else. The MBP is long since obsolete and gets kept around for a “Oh, I have this one weird legacy thing that needs MacOS…” device, and I’ve no plans to go back to them - even though, as noted earlier, I think the M series chips are the most exciting bits of hardware to come out of the computing world in the last decade or two, and the M series MacBook Pros are literally everything I want in a laptop. Slab sided powerhouses with actual ports. I just no longer trust Apple to do that which they’ve done in the past - they demonstrated that they were willing to burn all their accumulated privacy capital in a glorious bonfire of not implementing an awful idea. Weird as hell. I’ve no idea what I’m going to do when this phone is out of OS support. Landline, maybe.
I followed this basic plan when I went to UNSW to do a co-op on seL4, Concrete Semantics is a really solid textbook although I found myself not really grokking how to navigate between different styles of proof technique when confronted with a massive goal stack in some “real world” proofs I tried to do. Proof Engineering is a lot of fun!
You are so lucky. UNSW is one of the meccas of seL4, and Isabelle in general. I struggle to get proofs any longer than one line most of the time! But yea, it’s surprisingly fun - much like a puzzle.
Curious to know what materials on real proof engineering you went through after Concrete Semantics? I love the book, but have moved to Coq long ago mainly because of the lack of Isabelle-based material that describes practical engineering techniques.
To an outsider like me, it looks like Emacs development sped up in recent years. LSP and Tree-sitter integrations are especially noteworthy. It’s very impressive.
Piggybacking on this thread: what’s the current state of Emacs when it comes to remote development?
I’m aware of TRAMP but what I’m looking for is more complex.
I’d like a remote machine do most of the work (e.g. compilation, debugging, running a binary, code search). At the same time I’d like the text editing experience to not suffer the network latency so I’d like the client to run locally.
What are my options? Do you have any tried workflows?
It depends a lot on the language you are aiming to work with. Some modes have excellent TRAMP support, and if editing remote files they will fire a remote LSP, compiler / interpreter, etc. Others do not provide TRAMP support at all.
If your favorite major mode does not support TRAMP, one possibility is perhaps to use mosh instead of SSH and run the whole emacs remotely. This can reduce the impact of network latency.
It depends a lot on the language you are aiming to work with. Some modes have excellent TRAMP support, and if editing remote files they will fire a remote LSP, compiler / interpreter, etc.
That’s neat, I didn’t know that. I will check it out, thank you!
In my case it’s mostly Rust, Python, Go and sometimes C++.
The python-mode that ships with Emacs works really well with TRAMP, i.e. it fires a remote terminal, etc. I think all popular Python packages, such as anaconda-mode, build on top of it. So you are covered in that front.
I have never tried remote development using the other languages you mentioned.
I don’t think there’s one true easy option for that. Tramp is great but it’s possible individual libraries/modes will have buggy support. Editing over ssh is great if you don’t mind that. Honestly with something like the kitty terminal using emacs over ssh looks great and works for everything except actual inline images (although kitty can display those on it’s own, but emacs doesn’t know how to tell kitty to draw images… yet).
The venerable option of X11 forwarding can work, if latency is low.
Another option that I’ve seen recommended is to basically run emacs gtk with an HTML5 renderer and access via web browser. I haven’t tried it but allegedly there’s a PGTK (pure gtk) branch that has been merged somewhere and since GTK has a method to render to HTML5 you can take advantage of that: https://www.reddit.com/r/emacs/comments/rj8k32/the_pgtk_pure_gtk_branch_was_merged/
Personally I’d just go with either kitty ssh or emacs with remote desktop such as chrome remote desktop or nomachine (as I understand it nomachine is basically a proprietary version of X11 forwarding that’s actually usable for non-trivial applications). I use it every day.
I do this every day for work inside tmux+mosh; mosh does a pretty good job of papering over network latency issues to the point where they’re basically undetectable in my experience. But I’m always connecting to a host in the same city as I’m located so if you want to like … cross an ocean or a continent this may not be viable.
I’d like a remote machine do most of the work (e.g. compilation, debugging, running a binary, code search). At the same time I’d like the text editing experience to not suffer the network latency so I’d like the client to run locally.
Whereas others responding would run Emacs in SSH, I guess I would run SSH either in Emacs (in ansi-term-mode) or in a separate terminal emulator alongside Emacs and run the compilation (etc.) commands in the SSH session. If you run those commands with key bindings, I imagine the bindings could be changed to send the commands to the SSH session buffer (if running SSH in Emacs), although I personally have not tried to write programmatically into a term-mode buffer.
I’ve used every 29.1 pretest and rc across Windows, Mac, and Linux (Ubuntu, Debian, Manjaro, and Pop!_OS) and I’ve encountered no majors issues in the last few months. I’ve run these commands more than I’ve ever done before so maybe I will remember them this time lol
Really happy to see this release. Can’t wait to see all the new modes adopting tree-sitter. Haven’t been this excited about an Emacs release in a while! Looking forward to the day when this is the default Emacs on most Linux Distros but that will take a couple years
Emacs has made incredible progress since the late 2000s. At the time, you had to manage package libraries and versions manually. Plus, there was a lot of glue code you had to copy-paste into ~/.emacs to get it all working. For example, setting up Emacs for Ruby on Rails was quite hard. The outcome was fragile and often broke with updates.
With ELPA and use-package, everything has become much more streamlined, and as a consequence a very rich package ecosystem has emerged. My only complaint right now is that many packages still require a bit of ~/.emacs code to get up and running. Plus, documentation about how to mix and match packages to get IDE-like features is not great. The best source for that is, paradoxically, Doom Emacs. IMHO, this scares beginners away compared to VS Code, which is a shame.
I still remember the day when I read Your Text Editor Is Malware, I removed all the Emacs packages and manually git cloned or copy-pasted them to get some illusion of safety.
I guess the primary benefit by not using a package manager is getting a better understanding of their dependencies.
Yup. My new employer aims to ship CHERIoT products (Microsoft wants to use it in some places but not where users can see it). I’ll share more details in October. I’ll be hiring probably around December.
It’s security issues exactly like these (as well as a few other not mentioned such as package signing or possibly better SELinux support) that have kept us from investing in nix (government sector). Many of these types of things would need to be solved for us to be able to use nix in production.
For some of the issues like the current pull request model and packaging review I’m doubtful anything will change enough in the near term which is super unfortunate because of the potential nix brings to the table.
IMHO, thanks to its declarative nature, Nix is uniquely positioned to implement some user-friendly form of role-based access control and isolation. There are some efforts to support bwrap and AppArmor. SELinux is another option. I tried to push for things in this direction during some Nix meetings, but there are some really young contributors with zero engineering experience that think it is a bad idea because it’s incovenient and nobody uses it…
Great point as well. I am the official maintainer of a dozen packages and the current pull request model is a bit broken. Very often package source gets updated upstream. Nix bots update the source and create a PR for me to review. Typically, some other person rushes to push it without maintainer agreement. It looks like many GitHub users are trying to hoard many “contributions” to enhance metrics on their profile, which is valuable towards getting job interviews. This is scary, as malicious code can easily creep in.
Note that the PR and packaging reviews are for nixpkgs, not nix.
If you want different outcomes for nixpkgs reviews or a subset curated with better reviews and all, and have access to government money, i would recommend reaching out to the Nix foundation?
The main reason it is this way is that we are short of people to work on it. This is solvable with money. A support contract, signed with an org we would create for this purpose, is not an impossible thing to imagine.
But ofc it means actually investing in this.
I don’t disagree but pragmatically speaking it’s not that simple. For example, I’m one of two contractors on a specific team. Nix (the whole ecosystem) could provide real value to the struggles that we face daily. But using Nix in production, is an absolute non-starter at the moment due these style security issues.
Neither I, nor my team, have direct access to “government money,” we’re on a fixed contract. We also can’t just send money to sponsor work on nixpkgs. We need an actual organization that we can form a contract with for a billable service (basically all “purchases” above a particular threshold are actually contracts). i.e. Most of our infrastructure is RHEL and no-one bats an eye at spending many tens of thousands on RHEL support and subscriptions.
But it also seems like this type of offering is something the Nix community would absolutely oppose because it would require a non-community based org able to drive work and paid employees on timelines with SLAs, etc. Every time I see DetSys propose something it’s met with all kinds of ire about, “We can’t let nix be taken over by a corporation!” (there are lots of DetSys supporters too, to be clear)
Unfortunately too, it’s a chicken and egg problem at the moment. Even if for example the Nix Foundation (or whomever) started selling support contracts, we couldn’t immediately buy it because at present those security issues aren’t solved so we couldn’t yet put it in production. And if it can’t go in production we can’t purchase support. Additionally, being a community based project, there is disagreement on how, or even if the issues we care about should be solved.
So even hiring another contractor dedicated solely to nixpkgs isn’t feasible. Even ignoring the usual government red tap that makes anything take three times as long as you’d think (modifying a contract, requiring new bids, the convoluted hiring process, etc.), that one individual most likely can’t realistically affect the underlying security issues we’re talking about. Even nixpkgs review as others have mentioned, because unless somehow this new hire was able to instantly get merge rights their PRs would sit just like everyone else’s. Of course people will say, “Just hire someone already working those issues!” well, show me one of those individuals that has (or can get) a US security clearance, and is available for non-remote work in the US once a contract modification was approved in 12-18 months and I would genuinely love to talk to them! (Seriously…if that type of person exists I would be able to use them in all kinds of settings even if the nix stuff wasn’t viable).
It’s super frustrating down here where face daily challenges that we see a potential solution to.
How much does an end user can feel any of this?
I’ve not ever had a moment where I felt like “I wish my browser was faster”
It is usually the Internet
Without deep inspection it’s often hard to tell whether it’s the browser/website, or network latency, that is causing any visible delay - it is possible that you might be ascribing e.g. JS execution time to “the internet” on some sites.
I guess it is possible, but then 9/10 everything works fast on the good Internet days. It is only when Internet is slow that I ever start to moan about how everything is slow on a computer.
My daily driver is a humble 10-year-old NUC (i5-4250U).
Startup and pageload times have steadily improved during the last ~5 years, while my setup has stayed unchanged (XMonad + Firefox + uBlock).
It now feels really snappy. Most things are instant. I just wish there was a decent Vimperator replacement, as things have regressed in that area.
The Vim options aren’t bad… that is until you want something that works on built-in pages for settings, view source, raw text, etc. 😃
I am not saying there haven’t been noticeable perf improvements in browser history.
However, I think we are a point of significant diminishing returns. I am struggling to imagine that we are going to get measurable (from consumer perspective) performance improvements moving forward.
Many years ago, I was at a talk by Robin Milner where he argued that artificial intelligence is the wrong goal and that we should focus on augmented intelligence. Making computers do things that humans can do is not especially useful, making computers and humans able to do things that neither can do in isolation is hugely beneficial. Things like Copilot fit well into that lens, they don’t replace the human they let the human accomplish more.
To the notes at the end, I don’t find it worrying that an LLM can reproduce college essays, at least in the sense that’s implied. I see this as evidence that these forms of assessment are not measuring the right thing. I hope LLMs will be a disaster for the kind of assessment that doesn’t require original thinking yet purports to measure that faculty.
I agree. When these LLMs reach such high scores on standardized school/university tests, the shocking thing is not how far computers advanced, but how primitive our assessment of skill truly is. That it can be fooled by what amounts to a probabilistic mechanism that generates likely chains of tokens. That is not the kind of skill and resourcefulness you look for when you’re hiring people. True resourcefulness is navigating uncharted waters, not doing what is familiar but doing what is logical, given the circumstances.
It’s tricky. When you design an assessment there are four key things you need to think about:
A lot of university exams don’t even start with a construct against which they can measure validity. They have some aggregate hand waving towards impact (do people who graduate our course get good jobs and do well in them?) but often the sample sizes are too low. They do care about reliability because that’s the kind of thing that they need to demonstrate for accreditation, but only very loosely. They care a lot about practicality because the people marking assessments are not doing that full time, they’re also doing research.
Even with those caveats, a number of the things where LLMs do well are the kind of assessments that are intended to drive learning rather than give a final score. They are intended to tell the student what they need to study more. Cheating at these is like cheating at exercise.
I wasn’t at the talk but I think I saw either a recording of it, or he made that point in a later talk that I saw, and it was a pretty defining moment for my outlook on programming, and on technology in general. Based on that, and on my personal observations, I also think rumours of programming being on its way to the urn because of “AI” (by which commenters usually mean LLM) are greatly exaggerated. This article is probably a good example: it has a few good ideas, but the examples are tone-deaf.
I don’t remember where I read it first (I think Norvig quotes it in his big book on the topic, but I mostly skimmed it – my interest in AI is mostly confined to writing things that allow people who are better at math than I am write AI tools) but at some point, someone noted that mankind finally achieved its ancient dream of flying when it stopped trying to emulate the flight of birds, and tried to make things that fly starting from the principles of flight but without attempting to emulate the form of flight.
The examples in this article miss that: they get hung up on code monkey “tasks” (which may ultimately be fixed by incremental progresses in LLMs; ChatGPT 4 fares better on a lot of things, who knows what ChatGPT 6 will be able to do) or pointless programming puzzles. With any luck, something good may come out of that, like the death of interview programming puzzles, but that’s IMHO that’s not where the potential of LLMs lays.
I’m (slowly – the web is really not my platform) writing a tool that uses LLMs for very practical problems. tl;dr wife runs a marketing agency, I’m writing a tool that assists with the analysis of various types of promotional text. It’s very much an analysis tool; it has an interface that vaguely alludes to virtual assistants but the interaction is not chat-driven at all.
After hacking at it for a couple of evenings I’m fully convinced that LLMs will not spell the end of programming, and I’m really enthusiastic about what they can do:
The examples in the article are relevant in one way – I’ve found LLMs to be remarkably good at doing things that otherwise require tedious and somewhat “machine-like” human effort. For example, despite extracting and correlating a bunch of data from freeform text, and then showing it in standard format, my code has basically no serialization/deserialization logic. If I need ideas extracted from a text, and I need to hand them off in JSON format to the UI layer, I just request them in JSON format. If I need to show formatted text, I just request it in Markdown format. It’s not foolproof: chatgpt-3.5 occasionally hands me invalid JSON or tries to be nice and say “Here’s your JSON first”, so there’s some basic sanitizing logic in there; and there are security implications to it that I haven’t fully come to terms with. However, these look like problems that are perfectly tractable between incremental improvements in LLM (or, for that matter, some format awareness) and some real-life experience.
This part of writing an application may go the way of the Dodo – all that code that takes these two JSON objects and produces this other JSON object in a slightly different format, or takes this CSV document uploaded by the customer and produces this standard BOM table. But bloody hell, good riddance, if anyone dreads a future in which we’ll have to do less CRUD and object mapping, they’re suffering from Stockholm syndrome.
Seeing how prescient Milner was in general, I’ll go ahead and agree with him.
I think things could head in this direction? LLM-generated code is probably difficult to trust. There is some interesting work on synthesis based on contracts / advanced type systems using SAT/SMT. I expect both approaches might converge. We may end up designing programs, with AI helping to fill in the gaps.
Some things are. This is explicitly the goal of copilot. I am not convinced that it’s going in the right direction though because it’s acting as a glorified autocomplete and if typing is the bottleneck when programming then I’m doing something wrong. The kinds of things that I would love to see from LLMs are:
The main thing here is that they’re all low stakes: it won’t break the code if the LLM is wrong (except the refactorings, but that can be coupled with testing) but it will make the output much nicer for the same human investment.
assuming that the human brain is not the maximum possible intelligence a mind can have, and that artificial intelligences can surpass our intelligence by orders of magnitude, and that they can be run on faster processors with larger data stores, that AIs could be reproduced with a simple ctrl-v ctrl-p– the question should not be “what is AI good for?”, but “extrapolating current trends, how much longer will humans be useful for anything at all?”
That is probably true, though it may be that it devolves into discussions about forms of intelligence. The human brain is an interesting balance of compute vs I/O and it may be that increasing compute power alone is not useful, increasing compute and I/O gives something that is unrecognisable. Given that we currently have a sample size of one for building models of kinds of intelligence, there’s a lot of margin for error in anything that we build.
That’s a nice hypothetical but no one knows how to build one that even reaches the level of a human yet. The article shows problems that young children can solve but that state of the art LLMs can’t. To exceed by orders of magnitude, they’d first have to reach parity.
That said, there are some things that computers can already do orders of magnitude faster than humans. They can compute the sum of a list of integers many orders of magnitude faster than humans, for example. A human with a spreadsheet can achieve far more than a human without a computer, but the spreadsheet by itself can achieve nothing without human agency framing the problems. There are a lot of places where human+computer could be vastly more useful now than they are, but are being overlooked in the rush to make computer-without-human systems.
Again, that’s also not clear. Human brains are probably not quantum computers, but they are highly connected neural networks. Neurons in the brain can connect to several thousand other neurons. Transistors on silicon chips can connect to single digits of other transistors. Simulating this with matrix multiplication is not space efficient and slows down as the connectivity grows (especially when you use back propagation to represent feed-backwards neural networks). Adding larger data stores increases latency.
So, your argument starts with three axioms, none of which is proven and at least one of which may not be true in the sort to medium term. Logical arguments that start from axioms that are not generally helpful.
Extrapolating from current trends, forever. That may not be good extrapolation because this kind of development often happens in bursts. Extrapolating from the difference engine, humans would be useful for menial calculation for a long time, but extrapolating from the first electronic computers gave a clear end point for that utility. AI systems running on quantum computers may be able to express forms of conscious intelligence that are so far beyond humans that they’re unrecognisable, given some clever bit of mathematics that no one has thought of yet.
I think that you’ve begged the setup. What is intelligence? Or, at least, what does it mean to compare intelligences? Is there a lattice of intelligence?
I always asked myself, ever since i got introduced to prolog at the early stages of my university module theoretical computer science and abstract datatypes - what would i use prolog for and why would i use it for that?
I know two use cases where prolog is used earnestly, both deprecated these days:
Gerrit Code Review allowed creating new criteria a change must fulfill before it can be submitted. Examples
SPARK, an Ada dialect, used prolog up to SPARK2005 (paper). Out of the formal verification annotations and the Ada code it created prolog facts and rules. With those, certain queries passed if (and only if) the requirements encoded in those annotations were satisfied. They since moved to third party SAT solvers, which allowed them to increase the subset of Ada that could be verified (at the cost of being probabilistic, given that SAT is NP-complete: a true statement might not be verified successfully, but a false statement never passes as true), so prolog is gone.
Datalog, which is essentially a restricted Prolog, has made a bit of a resurgence in program verification. There are some new engines like Soufflé designed specifically by/for that community. Not an example of Prolog per se, but related to your point 2.
Yes, Datalog is heavily used for building state-of-the-art static analyzers, see https://arxiv.org/abs/2012.10086.
This is a great comment, I never knew about the Gerrit code review criteria.
A way I’ve been thinking about it is what if my database was more powerful & less boilerplate.
A big one for me is why can’t I extend a table with a view in the same way prolog can share the same name for a fact & a predicate/rule. Querying prolog doesn’t care about if what im querying comes from a fact (table) or a predicate (view).
This in practice i think would enable a lot of apps to move application logic into the database, I think this is a great thing.
The industry as a whole disagrees with this vehemently. I’m not sure if you were around for the early days of RDBMS stored procedure hell, but there’s a reason they’re used fairly infrequently.
What went wrong with them?
It’s nearly impossible to add tests of any kind to a stored procedure is the biggest one, IMO.
We actually do stored procedures at work & test them via rspec but it sucks. Versioning them also sucks to deal with. And the language is terrible from most perspectives, i think primarily it sucks going to a LSP-less experience.
I think to me though the root suckiness is trying to put a procedural language side by side a declarative one.
This wasn’t what I was saying with views.
I do think databases could be more debuggable & prolog helps here because you can actually debug your queries with breakpoints and everything. Wish i could do that with sql.
EDIT: but we continue to use stored procedures (and expand on them) because its just so much faster performance-wise than doing it in rails, and I don’t think any server language could compete with doing analysis right where the data lives.
Stored procedures can absolutely be the correct approach for performance critical things (network traversal is sometimes too much), but it also really depends. It’s harder to scale a database horizontally, and every stored procedure eats CPU cycles and RAM on your DB host.
I agree, prolog != SQL and can be really nice which may address many of the issues with traditional RDBMS stored procedures.
Yeah. DBs typically have pretty horrible debugging experiences, sadly.
I feel that that this is a very US-coastal point of view, like one that is common at coastal start-ups and FAANG companies but not as common elsewhere. I agree with it for the most part, but I suspect there are lots of boring enterprise companies, hospitals, and universities, running SQL Server / mostly on Windows or Oracle stacks that use the stored procedure hell pattern. I would venture that most companies that have a job title called “DBA” use this to some extent. In any case I think it’s far from the industry as a whole
Nah, I started my career out at a teleco in the Midwest, this is not a SV-centric opinion, those companies just have shit practices. Stored procedures are fine in moderation and in the right place, but pushing more of your application into the DB is very widely considered an anti-pattern and has been for at least a decade.
To be clear, I’m not saying using stored procedures at all is bad, the issue is implementing stuff that’s really data-centric application logic in your database is not great. To be fair to GP, they were talking about addressing some of the things that make approaching thing that way suck
@ngp, but I think you are interpreting
somewhat narrowly.
Sure we do not want stored procs, but moving Query complexity to a database (whether it is an in-process-embedded database, or external database) is a good thing.
Queries should not be implemented manually using some form of a ‘fluent’ APIs written by hand. This is like writing assembler by hand, when optimizing compilers exists and work correctly.
These kinds of query-by-hand implementations within an app, often lack global optimization opportunities (for both query and data storage). If these by-hand implementations do include global optimizations for space and time - then they are complex, and require maintenance by specialized engineers (and that increases overall engineering costs, and may make existing system more brittle than needed).
Also, we should be using in-process databases if the data is rather static, and does not need to be distributed to other processes (this is well served by embedding prolog)
Finally, prolog-based query also includes defining ‘fitment tests’ declaratively. Then prolog query responds finding existing data items that ‘fits’ the particular fitment tests. And that’s a very valuable type of query for applications that need to check for ‘existence’ of data satisfying a set of, often complex, criteria.
Databases can also be more difficult to scale horizontally. It can also be more expensive if you’re paying to license the database software (which is relatively common). I once had the brilliant idea to implement an API as an in-process extension to the DB we were using. It was elegant, but the performance was “meh” under load, and scaling was more difficult since the whole DB had to be distributed.
I have a slightly different question: does anybody use prolog for personal computing or scripts? I like learning languages which I can spin up to calculate something or do a 20 line script. Raku, J, and Frink are in this category for me, all as different kinds of “supercalculators”. Are there one-off things that are really easy in Prolog?
I’d say anything that solves “problems” like Sudoku or these logic puzzles I don’t know the name of “Amy lives in the red house, Peter lives next to Grace, Grace is amy’s grandma, the green house is on the left, who killed the mayor?” (OK, I made the last one up).
When I planned my wedding I briefly thought about writing some Prolog to give me a list of who should sit at which table (i.e. here’s a group of 3, a group of 5, a group of 7 and the table sizes are X,Y,Z), but in the end I did it with a piece of paper and bruteforcing by hand.
I think it would work well for class schedules, I remember one teacher at my high school had a huge whiteboard with magnets and rumour was he locked himself in for a week before each school year and crafted the schedules alone :P
The “classical” examples in my Prolog course at uni were mostly genealogy and word stems (this was in computer linguistics), but I’m not sure if that would still make sense 20y later (I had a feeling in this particular course they were a bit behind the time even in the early 00s).
This class of problems has a few different names: https://en.wikipedia.org/wiki/Zebra_Puzzle
Wonder if it would be good for small but intricate scheduling problems, like vacation planning. I’d compare with minizinc and z3.
I’d be interested to see a comparison like this. I don’t really know z3, but my impression is that you typically call it as a library from a more general-purpose language like Python. So I imagine you have to be aware of how there are two separate languages: z3 values are different than Python native values, and some operations like
if/and/orare inappropriate to use on z3 values because they’re not fully overloadable. (Maybe similar to this style of query builder.)By contrast, the CLP(Z) solver in Prolog feels very native. You can write some code thinking “this is a function on concrete numbers”, and use all the normal control-flow features like conditionals, or maplist. You’re thinking about numbers, not logic variables. But then it works seamlessly when you ask questions like “for which inputs is the output zero?”.
Update: I have fallen in love with Picat for solving this kind of problem.
It’s really good for parsing thanks to backtracking. When you have configuration and need to check constraints on it, logic programming is the right tool. Much of classical AI is searching state spaces, and Prolog is truly excellent for that. Plus Prolog’s predicates are symmetric as opposed to functions, which are one way, so you can run them backwards to generate examples (though SMT solvers are probably a better choice for that today).
Prolog is both awesome and terrible for parsing.
Awesome: DCGs + backtracking are a killer combo
Terrible: If it fails to parse, you get a “No”, and nothing more. No indication of the row, col, falied token, nothing.
That subjectively resembles parser combinator libraries. I guess if you parse with a general-purpose language, even if the structure of your program resembles the structure of your sentences, you give up on getting anything for free; it’s impossible for a machine to say “why” an arbitrary program failed to give the result you wanted.
You can insert cuts to prevent backtracking past a certain point and keep a list of the longest successful parse to get some error information, but getting information about why the parse failed is hard.
And then your cuts are in the way for using the parser as a generator, thus killing the DCG second use.
I have used it to prototype solutions when writing code for things that don’t do a lot of I/O. I have a bunch of things and I want a bunch of other things but I’m unsure of how to go from one to the other.
In those situations it’s sometimes surprisingly easy to write the intermediary transformations in Prolog and once that works figure out “how it did it” so it can be implemented in another language.
Porting the solution to another language often takes multiple times longer than the initial Prolog implementation – so it is really powerful.
You could use it to define permissions. Imagine you have a web app with all kinds of rules like:
You can write down each rule once as a Prolog rule, and then query it in different ways:
Like a database, it will use a different execution strategy depending on the query. And also like a database, you can separately create indexes or provide hints, without changing the business logic.
For a real-world example, the Yarn package manager uses Tau Prolog–I think to let package authors define which version combinations are allowed.
When you have an appreciable level of strength with Prolog, you will find it to be a nice language for modeling problems and thinking about potential solutions. Because it lets you express ideas in a very high level, “I don’t really care how you make this happen but just do it” way, you can spend more of your time thinking about the nature of the model.
There are probably other systems that are even better at this (Alloy, for instance) but Prolog has the benefit of being extremely simple. Most of the difficulty with Prolog is in understanding this.
That hasn’t been my experience (I have written a non-trivial amount of Prolog, but not for a long time). Everything I’ve written in Prolog beyond toy examples has required me to understand how SLD derivation works and structure my code (often with red cuts) to ensure that SLD derivation reaches my goal.
This is part of the reason that Z3 is now my go-to tool for the kinds of problems where I used to use Prolog. It will use a bunch of heuristics to find a solution and has a tactics interface that lets my guide its exploration if that fails.
I don’t want to denigrate you, but in my experience, the appearance of red cuts indicates deeper problems with the model.
I’m glad you found a tool that works for you in Z3, and I am encouraged by your comment about it to check it out soon. Thank you!
I’m really curious if you can point me to a largish Prolog codebase that doesn’t use red cuts. I always considered them unavoidable (which is why they’re usually introduced so early in teaching Prolog). Anything that needs a breadth-first traversal, which (in my somewhat limited experience) tends to be most things that aren’t simple data models, requires red cuts.
Unfortunately, I can’t point you to a largish Prolog codebase at all, let alone one that meets certain criteria. However, I would encourage you to follow up on this idea at https://swi-prolog.discourse.group/ since someone there may be able to present a more subtle and informed viewpoint than I can on this subject.
I will point out that the tutorial under discussion, The Power of Prolog, has almost nothing to say about cuts; searching, I only found any mention of red cuts on this page: https://www.metalevel.at/prolog/fun, where Markus is basically arguing against using them.
So when does this happen? I’ve tried to learn Prolog a few times and I guess I always managed to pick problems which Prolog’s solver sucks at solving. And figuring out how to trick Prolog’s backtracking into behaving like a better algorithm is beyond me. I think the last attempt involved some silly logic puzzle that was really easy to solve on paper; my Prolog solution took so long to run that I wrote and ran a bruteforce search over the input space in Python in the time, and gave up on the Prolog. I can’t find my code or remember what the puzzle was, annoyingly.
I am skeptical, generally, because in my view the set of search problems that are canonically solved with unguided backtracking is basically just the set of unsolved search problems. But I’d be very happy to see some satisfying examples of Prolog delivering on the “I don’t really care how you make this happen” thing.
As an example, I believe Java’s class loader verifier is written in prolog (even the specification is written in a prolog-ish way).
class loader verifier? What a strange thing to even exist… but thanks, I’ll have a look.
How is that strange? It verifies that the bytecode in a function is safe to run and won’t underflow or overflow the stack or do other illegal things.
This was very important for the first use case of Java, namely untrusted applets downloaded and run in a browser. It’s still pretty advanced compared to the way JavaScript is loaded today.
I mean I can’t know from the description that it’s definitely wrong, but it sure sounds weird. Taking it away would obviously be bad, but that just moves the weirdness: why is it necessary? “Give the attacker a bunch of dangerous primitives and then check to make sure they don’t abuse them” seems like a bad idea to me. Sort of the opposite of “parse, don’t verify”.
Presumably JVMs as originally conceived verified the bytecode coming in and then blindly executed it with a VM in C or C++. Do they still work that way? I can see why the verifier would make sense in that world, although I’m still not convinced it’s a good design.
You can download a random class file from the internet and load it dynamically and have it linked together with your existing code. You somehow have to make sure it is actually type safe, and there are also in-method requirements that have to be followed (that also be type safe, plus you can’t just do pop pop pop on an empty stack). It is definitely a good design because if you prove it beforehand, then you don’t have to add runtime checks for these things.
And, depending on what you mean by “do they still work that way”, yeah, there is still byte code verification on class load, though it may be disabled for some part of the standard library by default in an upcoming release, from what I heard. You can also manually disable it if you want, but it is not recommended. But the most often ran code will execute as native machine code, so there the JIT compiler is responsible for outputting correct code.
As for the prolog part, I was wrong, it is only used in the specification, not for the actual implementation.
I think the design problem lies in the requirements you’re taking for granted. I’m not suggesting that just yeeting some untrusted IR into memory and executing it blindly would be a good idea. Rather I think that if that’s a thing you could do, you probably weren’t going to build a secure system. For example, why are we linking code from different trust domains?
Checking untrusted bytecode to see if it has anything nasty in it has the same vibe as checking form inputs to see if they have SQL injection attacks in them. This vibe, to be precise.
…Reading this reply back I feel like I’ve made it sound like a bigger deal than it is. I wouldn’t assume a thing was inherently terrible just because it had a bytecode verifier. I just think it’s a small sign that something may be wrong.
Honestly, I can’t really think of a different way, especially regarding type checking across boundaries. You have a square-shaped hole and you want to be able to plug there squares, but you may have gotten them from any place. There is no going around checking if random thing fits a square, parsing doesn’t apply here.
Also, plain Java byte code can’t do any harm, besides crashing itself, so it is not really the case you point at — a memory-safe JVM interpreter will be memory-safe. The security issue comes from all the capabilities that JVM code can access. If anything, this type checking across boundaries is important to allow interoperability of code, and it is a thoroughly under-appreciated part of the JVM I would say: there is not many platforms that allow linking together binaries type-safely and backwards compatibly (you can extend one and it will still work fine).
Honestly, I can’t really think of a different way, especially regarding type checking across boundaries. You have a square-shaped hole and you want to be able to plug there squares, but you may have gotten them from any place. There is no going around checking if random thing fits a square, parsing doesn’t apply here.
Also, plain Java byte code can’t do any harm, besides crashing itself, so it is not really the case you point at — a memory-safe JVM interpreter will be memory-safe. The security issue comes from all the capabilities that JVM code can access. If anything, this type checking across boundaries is important to allow interoperability of code, and it is a thoroughly under-appreciated part of the JVM I would say: there is not many platforms that allow linking together binaries type-safely and backwards compatibly (you can extend one and it will still work fine).
Well, how is this different from downloading and running JS? In both cases it’s untrusted code and you put measures in place to keep it from doing unsafe things. The JS parser checks for syntax errors; the JVM verifier checks for bytecode errors.
JVMs never “blindly executed” downloaded code. That’s what SecurityManagers are for. The verifier is to ensure the bytecode doesn’t break the interpreter; the security manager prevents the code from calling unsafe APIs. (Dang, I think SecurityManager might be the wrong name. It’s been soooo long since I worked on Apple’s JVM.)
I know there have been plenty of exploits from SecurityManager bugs; I don’t remember any being caused by the bytecode verifier, which is a pretty simple/straightforward theorem prover.
In my experience, it happens when I have built up enough infrastructure around the model that I can express myself declaratively rather than procedurally. Jumping to solving the problem tends to lead to frustration; it’s better to think about different ways of representing the problem and what sorts of queries are enabled or frustrated by those approaches for a while.
Let me stress that I think of it as a tool for thinking about a problem rather than for solving a problem. Once you have a concrete idea of how to solve a problem in mind—and if you are trying to trick it into being more efficient, you are already there—it is usually more convenient to express that in another language. It’s not a tool I use daily. I don’t have brand new problems every day, unfortunately.
Some logic puzzles lend themselves to pure Prolog, but many benefit from CLP or CHR. With logic puzzles specifically, it’s good to look at some example solutions to get the spirit of how to solve them with Prolog. Knowing what to model and what to omit is a bit of an art there. I don’t usually find the best solutions to these things on my own. Also, it takes some time to find the right balance of declarative and procedural thinking when using Prolog.
Separately, being frustrated at Prolog for being weird and gassy was part of the learning experience for me. I suppose there may have been a time and place when learning it was easier than the alternatives. But it is definitely easier to learn Python or any number of modern procedural languages, and the benefit seems to be greater due to wider applicability. I am glad I know Prolog and I am happy to see people learning it. But it’s not the best tool for any job today really—but an interesting and poorly-understood tool nonetheless.
I have an unexplored idea somewhere of using it to drive the logic engine behind an always on “terraform like” controller.
Instead of defining only the state you want, it allows you to define “what actions to do to get there”, rules of what is not allowed as intermediary or final states and even ordering.
All things that terraform makes hard rn.
Datalog is used for querying some databases (datomic, logica, xtdb). I think the main advantages claimed over SQL are that its simple to learn and write, composable, and some claims about more efficient joins which I’m skeptical about.
https://docs.datomic.com/pro/query/query.html#why-datalog has some justifications of their choice of datalog.
Datomic and XTDB see some real world use as application databases for clojure apps. Idk if anyone uses logica.
When I click this link, it downloads to my computer instead of opening in browser directly. I don’t like this
Sounds like a web browser configuration issue. On Firefox, it opens on a new tab.
Sounds really bad. This will make it hard to run non-mainstream platforms.
I guess regulators might step in and demand alternative modes of attestation, like they have done in case of iOS and the single-store monopoly. However, they are exceedingly slow at doing so. For instance, now it is impossible to do online banking in some places if you don’t run iOS or Android. Something as innocent as AOSP is not supported, even if you run the same banking app, due to the lack of SafetyNet attestation.
It’s also not clear to me that policymakers have any particular reason to care about non-commercial platforms or software modification as civil liberties issues. So we might not get the regulation we want…
Honestly not a bad time to start thinking about what the rules OUGHT to be in an ideal world. Even if we can’t get there anytime soon, knowing where we want to go has to help somehow.
The EU has a good reason to care. All of the big OS vendors are based in the US. If things require an attestation that only a US company can provide then this makes it impossible for any EU startup to ever grow to being a big company in this space.
This is especially true when you consider that things like the YouTube and Android are owned by the same US entity. If Google decides to require attestation to watch YouTube videos (so that they know that you aren’t using a client that skips ads, for example) then there is a fairly clear argument under existing monopoly law that they’re using their effective monopoly in one market to ensure that there can be no competition entering another market where they’re a significant player.
I think we need to learn a lot from the problems with DRM here. We pushed back on the technologies, rather than the uses. We didn’t block the technology in standards bodies (in part because there are some non-evil uses, such as access control within an organisation) and we didn’t get regulations on acceptable use. I’d love to see using DRM that prevents users from exercising fair use rights treated as vigilanteism and grounds for having copyright on the work in question revoked. Similarly, anyone using this kind of attestation to lock in clients to a particular platform should be subject to serious antitrust investigation.
The political leaders of the EU have a good reason to care that European keys find their ways into the TPMs of digital devices. They have no reason whatsoever to care about civil liberties of Europeans, or that people can run their own libre software on their devices. Quite the contrary - free computing is a threat to governing bodies, especially those that like to grow in size and power. The TPM menace will only grow worse as time goes on.
Yes, absolutely. Good thoughts.
My immediate vision is of a future where I end up having to literally drive to the bank to pay my bills because, eventually, I will no longer run a rights-infringing OS that happens to be the only one supported by online banking. It doesn’t even seem farfetched. I already am excluded from lots of software, games, and online services that require an OS I refuse to utilize, and the rate of that exclusion definitely seems to be accelerating quickly.
Yes, agreed. Quite distressing, but that’s the path we’re on and the route I’ll take as well.
I think it can be reduced to: shared mutable state is the root of all evil, and forbidding mutation is one sure way to prevent it.
This argument crops up once in a while. This is an interesting article from a while back: https://hillelwayne.com/post/theorem-prover-showdown/.
Mutable state is not “evil”.^ Shared mutable state is not “evil”. Yes, undisciplined use of either makes software harder to reason about. But there is nothing intrinsically “evil” about shared mutable state. It’s a fundamental component of the machine model that underlies our computers.
^ It’s meaningless to use terms like “evil” w.r.t. technology.
This reminds me that I’ve always though the technical term “pure” has unfortunate moralistic overtones.
And literally the source of all security holes that are buffer overflows, which is a huge percentage of them.
I agree with what you’re saying, but I don’t see the relation to the “let’s prove leftpad” series. What’s the relation?
Fair point. I wasn’t clear at all why the link is interesting. It talks about program correctness (which is a good part of the linked article) from a FP/IP perspective. Hillel’s article also talks about blanket statemens in the vein of the parent comment.
EDIT: Hillel’s article is about the issue you mentioned in your other comment in this thread, if it’s easier to prove programs correct in IP or FP.
Oh I get it. Let’s prove leftpad focused on algorithms that are generally implemented imperatively.
While I also prefer functional programming, if we talk about formal verification, in some cases imperative code is easier to prove correct.
If we consider static analysis, simple imperative languages are generally easier to deal with, especially from the toolbuilder perspective.
I’m not too familiar with formal verification (aside from TLA+ style); is there a reason imperative code is easier to prove correct? Is it primarily due to the tooling, or innate to the math backing formal verification?
Mainly asking because I was under the impression that functional languages stick far more closely to CS math, while imperative is less so.
For static analysis, I have to say I’m confused here. Strong type systems (a feature of many functional languages, but not necessarily) and pure functions seem like they would lend themselves far more easily to static analysis.
I mostly disagree.
There is a large gap in effort invested in static analysis tooling for imperative vs. functional programming; for a while people basically focused on just analyzing C code, and it shows (without saying much about the fundamental difficulty). (For example, SMT solvers became relatively good at numerical reasoning, and generally disappointing at reasoning on rich datatypes, but this is not because integer manipulations are easier, it is because early they focused on programs doing a lot of array indexing.)
My experience is that functional code in most cases has simpler invariants and specifications.
Most static analysis tools on imperative programs are meant to prove safety properties, typically the absence of undefined behaviors, or some relatively safe asserts. If we are talking about “proving correct”, we are talking full correctness. And there the state of the art seems much stronger for functional programs. Do we have any example of notable program with a full correctness proof, written from the start in an imperative style? Probably the two flagship examples of full verified programs are CompCert (a C compiler) and seL4 (a microkernel), CompCert is written in a very functional mix of Coq and OCaml, and seL4 is a Haskell program that is refined into a C implementation. I know of a few cases of verified programs that were written in an imperative style first, mostly in the crypto domain, because it was a design requirement to generate C code from the start (the HACL* stuff0.
(This point suffers from a dual of the bias argument of point (1): one could argue that most large verified programs are written in a functional style because most program-verification practitioners prefer functional programming. I don’t think this suffices to explain the gap, but it is of course worth keeping in mind.)
FP languages are overrated when it comes to proving full correctness. seL4 and CompCert were written at a pace of 2 LoC/person-day, which is utterly outclassed by IronFleet. That was done in the imperative Dafny and written at the blistering pace of 4 LoC/person-day.
Total correctness is just a really hard problem regardless of the paradigm you use.
(I’ve heard SPARK people claim they can do better than 4 loc/day, but I haven’t analyzed a large SPARK project yet.)
I’m not familiar with the IronFleet work, but here is section 6.2 of the “IronFleet: Proving Practical Distributed Systems Correct” paper (Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, Brian Zill; 2015):
It looks like the IronFleet authors agree with what I said above, and their verification approach is close, when it comes to implementation, to the one of SeL4: implement a functional program, then refine into an imperative program.
(One could make a qualitative distinction on whether the functional program merely serves as a model – as automata-style state models or is a “real implementation”, and I don’t know the status here.)
I’ve never heard of imperative code having any verification benefits. Do you have some examples / references for this?
A few years back I talked with the seL4 people and they had two things that made functional harder:
Interesting. I guess nothing is absolute huh.
I don’t have any open code to share, but some exceptions come from control and real-time systems I have worked in. Verifying state machines, which are a natural way to represent some control problems, and/or proving they satisfy time constraints, is sometimes easier with imperative code.
In general, I agree functional code is easier to prove correct thanks to referential transparency. I just stated there are some exceptions.
If you’re interested in any way in learning about proofs and formal verification, I can’t recommend Isabelle enough. I never proved anything in my life before using Isabelle, and now I’m able to do relatively non-trivial things in it.
I think it’s easier than all of the other proof assistants to get into, because the logic (HOL) is simpler, and is pretty much like ML / Haskell with a few additional concepts. The automation is also really good, and for a while you can get away with proving things with a one liner:
by auto, without understanding too much of what’s going on under the hood.I think that’s really important, because otherwise it’s really hard to achieve liftoff when you don’t know how to specify nor prove things. Proof automation allows you to focus a lot more on the specification side first, and then you can build on getting better at the actual act of proving over time.
How does Isabelle intersect with formal verification generally? I think I remember reading it’s used to prove things about the output assembly code or something?
The flagship example is the seL4 OS. They have a C parser which connects to a formal C semantics in Isabelle, so they verify actual C code against a functional correctness specification.
Then, and this is my personal favorite project, there’s also Cogent which is a language that compiles to C, but it uses the pattern of certifying compilation to produce a proof of correctness along with it. They’ve used this to implement verified file systems.
It was also used to verify several properties about WebAssembly, where the formalization found soundness errors in the type system that led to changes to the spec IIRC.
It also supports extraction, similar to Coq, where you can extract verified components to Haskell / OCaml, etc. I think the wasm project used this to extract a reference interpreter for testing.
The proofs for seL4 go even deeper (for Armv7): the seL4 team did binary verification, where they verified that the compiled object code corresponds to the C code that should have been compiled, eliminating the compiler from the trusted code base.
(though this isn’t done in Isabelle, they used SMT-techniques instead)
Indeed, it is a really nice theorem prover based on classical logic. Documentation is excellent: https://isabelle.in.tum.de/documentation.html
I am just missing some more practical Isabelle tutorials geared towards proving techniques for big software artifacts like seL4. Any suggestions?
Coq has great documentation in that regard. For instance: http://adam.chlipala.net/frap/frap_book.pdf
Coq has more users, there’s no getting around that. I assuming you know about Concrete Semantics, though that’s not really about large-scale verification. I’ve gotten a lot of information by reading seL4 papers about that.
Other than that, I use Isabelle to do exercises for any book. For example, I did it for Types and Programming Languages, and that was a great experience. The same should apply to FRAP and Software Foundations - they do have some Coq-specific content, but everything there can be formalized in Isabelle.
I think there’s a relative void for what you’re asking, for sure. Proof engineering is still very niche, and the already-small community is still fragmented.
I think this is slightly misleading. BEAM saves them the money and they like the affordances in Elixir. I was pretty surprised until I saw that their baseline was Ruby. BEAM is a lot slower than most low-level languages, but Ruby is well known to be painfully slow. Last time I looked at the language shootout game results, it was a quarte of the speed of Squeak (Smalltalk). Squeak is written to be flexible and understandable at the expense of performance, Ruby eliminates the features of Smalltalk that add the worse performance overhead and still manages to be slow.
Ruby is not too bad now compared to Smalltalk. One thing to keep in mind is that pre 1.9, Matz’s Ruby Implementation (MRI) was the de facto standard. And it was slow. Switching to a bytecode interpreter has improved performance: https://benchmarksgame-team.pages.debian.net/benchmarksgame/fastest/ruby.html
I’m not sure it’s only speed. Just by having cheaper parallelism (and ‘hanging’ connections) you can do a lot with the BEAM where a multi-threaded (or multi-proc) server in ruby would need a lot more memory (and probably CPU).
That’s true. I first used Erlang during my PhD and wrote code that ran on my single-core PowerBook and scaled linearly to the 64-processor (MIPS) SGI box that I deployed it on. I have never done that in any other language. Unfortunately, per core it ran at 1/10th the speed of the C version. I definitely couldn’t do it in a Smalltalk-family language like Ruby without some very rigid discipline that would remove most of the value such a language.
It would be interesting to look at a baseline like Pony, which is much faster for straight-line execution than BEAM.
It compounds too. A lot of things become easier like a long running pool of connections to your db, which makes the caching on postgres far more efficient as an example.
Cost of crashes are lower too, latency tend to handle high load better, etc etc. It compounds pretty fast into really tangible results.
I briefly tried NixOS. I love the idea, and having my configuration (which I try to keep simple) available right there is very nice. Unfortunately I hit a couple snags:
makeflavour I was using.I’m sure these could be fixed, perhaps even easily so. If I was more serious about Nix I would probably have pushed through, solved these, and contributed. I like Nix, and maybe I’ll come back some day. Right now unfortunately I have other priorities, so I went back to Ubuntu.
That said, I’m not ruling out revising Nix in a few years.
I had much the same experience! That was almost 4 years ago now, though, and this time around it’s clicked.
I think the main thing Nix gives me despite having to work around things like these is that the workarounds are (in their own way, at least) permanent. Once you get the config into a given state, it’s a done deal, and this is super valuable to me as someone who uses a number of different “personal” machines in different contexts. I find myself putting more time into the refinement of my (human interface) systems because it’s not just sitting in a dotfile, or a git-backed dotfile, or a (…), but something structured and expressive enough to do ~anything. (like with patching fish(1) in this post.)
Adding the time dimension to system configuration in a legible way means you are building something, not just tweaking nobs, and though I didn’t think I’d ever appreciate the need, having implemented it, I’m very content.
Nix is a whole new paradigm, so there’s a lot of stuff to get used to to be idiomatic. Unfortunately the documentation sucks, and the maintainers seem to disagree that it sucks, saying that it’s irreducible complexity (bull because Nix derivations are incredibly simple compared to other packaging systems when written idiomatically) or that people just have to get used to it (bull because it’s really effing hard to discover things when they are not hyperlinked together, or the tooling produces alien output).
Well it can always be better in the future…
…or not.
Shame. One thing’s for sure, I probably won’t come back until documentation gets better. Not just the general stuff (which to be honest looked pretty good), but the boring stuff like how to discover the existence of a particular helper function, whose apparent absence were a reason for my departure. Or the complete description of the relevant options for any particular package I try to include in my configuration. I can’t be expected to look at the source package, I haven’t even stumbled upon how to find and read it.
While we’re at it, one more thing that caused me to leave: using
?=assignment inmake. I did to assign standard variables likeCCandCFLAGSbecause users are supposed to be able to override this with environment variables, and, as far as I could tell, it’s also a convention to tell users “go ahead, you can override this safely”. When I used the regular=assignment, one user asked me if it was safe to change the compiler, they genuinely weren’t quite sure (and they understandably wouldn’t take chances with a crypto library).Problem is, stupid GNU Make ignores my default, even when the users don’t have their
CCorCFLAGSenvironment variables set. Why? Because there’s a build-in default, that an explicit default does not override (because it’s “already set”). So instead of my specified default (gcc -std=c99), we get justcc… well, that’s what the GNU documentation says, but in reality I gotc99.I got really confused to be honest: why was Make truncating my option? Does it ignores whatever is between
?=and=or something? And of course my system didn’t have thec99compiler, so I just gave up on the?=idea, thinking maybe it was a BSD thing……until I retried it on my fresh Ubuntu system. And what do you know, it worked! Well, not quite, GNU Make was as stupid as ever, and still used
c99by default despite me specifying another default. Same deal forCFLAGS. But this time, my system had an alias, which lead me to understand that really, this stupidity from GNU Make was intentional.Couldn’t have learned that from NixOS, though: it didn’t have that alias, so when I tried it there, I just thought there was “something special” going on that were confusing me, and just gave up on
?=for the time being.Which reminded me, NixOS doesn’t have a
/bin/enveither. In so many places I see that we should prefer#! /bin/env shand#! /bin/env python3over#! /bin/shor#! /usr/bin/python3. But that didn’t work with NixOS, so I ended up adding a hard link to the actualenvprogram (maybe configuration could have done that for me).I got a similar problem with
pkg-config: there is some setup to do before I can justsudo make installa pkg-config aware tarball and expectpkg-config --cflags my_tarballto work. Out of the box it doesn’t. Again, I made it work the ugly way, not quite knowing what the proper way was. (Though I suspect the proper way is to never just typesudo make installin the first place, but instead write a Nix package for this source code, which I didn’t know how to do.)All this to say, the GNU/Linux ecosystem has a lot assumptions baked in. Many of them are hard to guess, until we stumble upon a system, like NixOS, that breaks them. And boy does NixOS breaks a lot of such assumptions. So we need to either fix those breaks, or do things the Nix way even though the very software it packages does not play the same game. There’s a rather tall wall to climb, and I don’t know how.
This thing about maintainers allegedly thinking their documentation is fine? It’s worrying. Long term, it could even kill Nix and NixOS. I really hope it gets better.
About
env, it’s#!/usr/bin/env bash,#!/usr/bin/env python3etc./usr/bin/envis actually POSIX, I’ve never heard of anyone referring to/bin/env.Yeah, that one was my mistake (for just one script, all the others use
/usr/bin/env, that went unnoticed because Ubuntu (my previous system) actually conflates/binand/usr/bin.Now it’s all corrected and harmonised into one of the following:
(Hopefully my shell scripts stick to the old Bourne shell, without any Bash extension.)
I’ve never seen
/bin/envas opposed to/usr/bin/env, which NixOS does have.GNU (and I think BSD)
env‘s “canonical” home is/usr/bin, but lots of distros merged /usr/bin and /bin a long time ago which has caused various hardcoded paths to seep from one into the other.envhas always lived in/usr/bin, as far as I know, or in any case it’s been there for as long as I remember it; but it “feels” like something that ought to be in/bin, and/bin/envjust happens to work because/binis now a symlink to/usr/binalmost everywhere.Ah, I misremembered. I’m using I’m using
/usr/bin/envindeed almost everywhere… and botched one instance. Correcting now, thanks for the reminder.Except when you’re building! (
patchShebangs)I installed NixOS on my work laptop during the early stages of the pandemic, when I should probably have been doing something else but didn’t have any sanity left to do those things. Before that I had bounced off it a couple of times, much in the manner you describe. For what it’s worth the amount of snags that need figuring out seem to be bounded and they grow at a rate measured in years. So there is a hump to get over at first, but if you get over it the sailing is very smooth after that.
If anyone’s struggling with aspell, it’s a bit weird, but you install
(aspellWithDicts (dicts: [dicts.en]))and get all the English types included.I agree that
environment.systemPackages = [(pkgs.aspellWithDicts (dicts: [dicts.en]))]is nicer thanenvironment.systemPackages = [pkgs.aspell pkgs.aspellDicts.en], but you seem to be saying that it gives a different result? If so, how?If you install them separately, aspell doesn’t know the dictionaries are available since they’re completely separate paths. aspellWithDicts generates the correct merge/wrapper to bind them together. This is a usual problem with apps that require plugins.
Didn’t know about this method. What I found was a little different:
Only English dictionary I got from this one was US. I guess it’s an “oh but of course you’re using the old method” or something, but it’s the method I found, and searching failed to turn up the other one. Also, had I tried it blind, I would have imitated Python, and maybe come up with something like the following at best:
I mean, the
aspellWithDictspackage would have been a total unknown for me.Yeah, that one’s really not obvious. And not really documented as far as I can tell. Could be worth raising an issue.
This is something that requires a bit of readjustment to Nix and its way of doing things, as it does not rely on dynamic linking or uncontrolled environment variables.
All tools are composed by indicating subpackages with the appropriate helper function. There are helper functions for everything ranging from TeX to Emacs.
That’s less a Nix thing than a nixpkgs-specific thing. The discoverability of those helpers is awful. For example, if you just search
aspellon search.nixos.org/packages, you just getaspellandaspellDicts.*. There’s no indication that theaspellpackage includes a helper function for adding dictionaries.I agree. The problem right now is that Nix has no clear learning path. Even if you are willing to put a lot of effort, documentation is patchy and you end up needing to look at source. The split between flakes and channels makes this even more difficult. Guix is much more coherent.
There shouldn’t be a comma in that list; it would be
(aspell.withDicts (dicts: [dicts.fr dicts.en])).The coma would be easy enough to figure out (I have a similar list with Python), it’s the spelling of everything else that would have been a problem.
| Perl (sloccount) nagged me about my locales not being set up properly
Somewhat tangential to your post, but just fyi, there is exists a Go rewrite of sloccount, called loccount.
It is updated more than the original (sloccount seems to be unmaintained) and doesn’t generate the Perl warnings.
(With the
-cflag, it even generates the Cocomo model estimates, which may be inaccurate, but it’s still fun to read.)I’ve started using
sccinstead, it seems to give more details thanloccountwhile being much more up-to-date thansloccount.I love both Haskell and OCaml, and I have used them quite extensively.
My feel is that OCaml is on an upward trend. It is in the process of addressing, or has already addressed, some major pain points: multicore and better control of impurity (via effects). Plus, ML in general is gaining exposure with Rust, Swift and Scala. Interesting libraries are getting written, and there are lots of OCaml users in the formal methods community.
Haskell, on the other hand, seems to be declining. Some community leaders have moved elsewhere. The standard has become stagnant and the library ecosystem does not look very lively. There is no real effort to streamline the whole Haskell stack for industrial users, perhaps because the language wants to optimize for research.
It seems like Jane St is funding almost all non-academic OCaml compiler and runtime work?
That makes all the difference in the world … Getting like 5 really good people full time, is 1000x better than getting 100 people in their spare time (usually researchers)
Kind of reminds me of - https://discourse.elm-lang.org/t/costs-funding-in-open-source-languages/5722
e.g. JavaScript is a funded language because it’s attached to certain businesses, and I think the same is true of OCaml. Not saying that’s good or bad, but it appears to be the truth.
Also Tarides (supported by Tezos) and, of course, INRIA are doing real-world OCaml development, e.g. multicore.
I agree with you, having some full-time core developers makes a huge difference. I think it is a shame many big Haskell users are not giving a bit more back by funding such a core.
I mean, Haskell and Haskell tooling are generally so good that I’m often more annoyed than excited by new release (because if they changed anything there’s a small chance it got worse. Would be hard for it to get better…)
Where did such community leaders go?
Sadly, being a community leader doesn’t get you a job.
At least some of them, such as Simon Peyton Jones,¹ seem to be working on a new language named Verse:
¹ although SPJ appears still to be active with Haskell
Some of them went into crypto
I have started learning OCaml and am working through Real World OCaml.
Does anyone recommend any other tutorials or references?
The Functional Approach to Programming with Caml by Guy Cousineau and Michel Mauny is really good.
However, it is not an OCaml reference, but rather a functional programming textbook that overlaps with TAPL and other textbooks. It is a bit of Caml + PLT.
Actually, it uses Caml Light, which precedes OCaml. But examples should be quite trivial to translate. See: https://github.com/mauny/the-functional-approach-to-programming/tree/master
Thanks for the recommendation! I forked the repo and have started translating the examples.
Sounds like OCaml’s goals.
That’s a good point. Is OCaml basically Simple Haskell minus laziness?
What about industry usage? OCaml seems less popular, although both are niche languages and multicore might alter that trend.
It’s not really simpler, just slightly different. Not lazy, not pure, and object oriented. It’s the inspiration for a whole family of ocaml clones like swift, Scala, rust, etc
Sure, I know, I have programmed quite a lot in OCaml and SML.
Haskell was heavily influenced by Miranda, which was a lazy successor to ML, and also by SML. So they are all pretty close in the lineage tree of programming languages.
My question was a bit more practical, about the niche both are trying to fill, and actual usage.
It has much fewer possibilities for writing code that people who are not fluent in the language don’t understand, because it’s much more “wordy”, like other functional languages and less “what does this overloaded operator in this code-golfed line mean”?
not positive those three calamities were the only ones…
if there were funding and employment structures (e.g., cooperatives, unions, credit unions) that allowed community choice and control in a way that GPL allows for software… maybe there’d be options besides the company making police sticks.
Very happy to see cooperatives mentioned; I think that’s got to become a huge part of the FOSS ecosystem if we want to see FOSS economically stabilized. Currently working on a project for this and I hope it’ll be out in a few months.
Can you elaborate?
The FOSS Jolla / Mer Linux mobile has been discussing such an option to make application development sustainable.
Roughly speaking, if you want a FOSS project to grow beyond a one-person hobby project, then there are two paths typically acknowledged. One is to rely on donations; the other is to become a startup. Both have flaws. One rarely raises enough in donations to support flourishing software development. And becoming a startup often leads to investor pressure to go down the path of “open-core”, or “source-available” relicensing, or (if you had contributors sign a CLA) folding and going totally proprietary.
As an alternative, I think if FOSS developers formed worker cooperatives to support their projects, then they’d get more economic support than from donations, but without the negative investor pressure that comes from conventional VC-backed incorporation. But currently there’s not much help on how to form a cooperative, or manage it, nor really is there widespread understanding of what a cooperative is. To really help the FOSS movement, there should be an ecosystem of institutions to helping developers establish coops, manage them, and promote this course of action in the wider community. I’m trying to build a piece of this ecosystem right now.
I’d love to hear about that when it’s public!
It’s sometimes easy to forget that all of the software that we use is built and maintained by individuals. Even tools that feel like they’ve been around for ages. (Relevant XKCD: https://xkcd.com/2347/)
Does anyone know what this means for the project and community? Are other people able to take over management or was it a one man show? I remember an argument for neovim being that it was community driven whereas vim had a BDFL.
RIP Bram
https://groups.google.com/g/vim_dev/c/6_yWxGhB_8I/m/ibserACYBAAJ
Christian is a long time contributor (and co-maintainer) of Vim and has commit access to the GitHub repo. It looks like he will step up as lead maintainer.
It has been a very long time since Bram was the sole developer on Vim, many of the changes are contributed by the community (with some notable exceptions). Bram would always commit the patches, but I would be very surprised if Bram’s passing significantly impacts the project.
I’m glad that people have access and can continue the work. Very sad that Christian didn’t get a chance to meet him in person though. You never know how much time you have with people.
Right now the EU is slowly starting to acknowledge this problem and pours a bit of cash into critical projects that are underfunded / maintained by a few.
Interestingly, a foundation called NLnet has an important role in selecting projects that get funded. AFAIK, Bram was an employee of NLnet.
This does make me regret selling my M1 Mini. Apple pissed me off enough with the whole CSAM/on device scanning thing (along with a range of other things) that I got rid of it, at some substantial loss, figuring that the Linux projects on it wouldn’t come to anything useful (at the time, they were still working out some basic functionality). Asahi has come a long ways since then.
They’ve done a really, really good job with hardware reverse engineering, and have quite exceeded my expectations for what they’d accomplish - I’m glad to see it!
I’m curious as to why you regret selling the hardware. A company proposes awful spyware for it’s hardware which you respond by deciding to sell it’s product but now you experience regret because you can’t test out software that the same company is not supporting or encouraging in the slightest? What is it about Asahi that makes you want an Apple device? I know Apple makes good hardware but I don’t think the hardware is THAT good that some independently contributed software is a game changer for it. Especially when many other vendors make pretty great hardware that support the software.
I like ARM chips, and I utterly love what Apple has done with the SoC design - huge caches, and insane gobs of memory bandwidth. The performance out of it backs the theory I’ve run with for a while that a modern CPU is simply memory limited - they spend a lot of their time waiting on data. Apple’s designs prove this out. They have staggeringly huge L1 cache for the latency, and untouchable memory bandwidth, with the performance one expects of that. On very, very little power.
Various people have observed that I like broken computers, and I really can’t argue. I enjoy somewhat challenging configurations to run - Asahi on Apple hardware tickles all those things, but with hardware that’s actually fast. I’ve used a variety of ARM SBCs as desktops for years now - Pis, ODroids, I had a Jetson Nano for a while, etc. They’re all broken in unique and novel ways, which is interesting, and a fun challenge to work around. I just didn’t expect Asahi to get this usable, this quickly.
I sold the M1 Mini and a LG 5k monitor at about a $1000 loss over what I’d paid for them (over a very short timescale - I normally buy computers and run them to EOL in whatever form that takes). I didn’t have any other systems that could drive the 5k, so it made sense to sell both and put a lower resolution monitor in the spot, but the M1/LG was still the nicest computer I’ve ever used in terms of performance, responsiveness, etc. And it would, in Rosetta emulation, run Kerbal Space Program, which was about the one graphically demanding thing I used to do with computers.
In any case, getting rid of it drove some re-evaluation of my needs/desires/security stances, and now I run Qubes on just about everything, on x86. Painful as it is to say, relative to my previous configurations, this all qualifies as “Just works.”
What did you replace it with? The basic Mac Mini M2 is really cheap now at ~$600. I run NixOS on a decade-old NUC, and it is tempting as a replacement. A good fanless x86 is easily 50% more and not nearly as energy efficient as the Mini.
However, right now one needs to keep macOS to do firmware updates. And AFAIK there is limited video output support on the M2.
An ASRock 4x4 Box 5000U system, with a 5800U and 64GB RAM. It dual boots QubesOS and Ubuntu, though almost never runs Ubuntu, and the integrated graphics aren’t particularly good (the theory had been that I could do a touch of light gaming in Ubuntu, but reality is that it doesn’t run anything graphically intensive very well). It was not a well thought out purchase, all things considered, for my needs. Though, at the time, I was busily re-evaluating my needs and assumed I needed more CPU and RAM than I really do.
I’m debating stuffing an ODroid H3+ in place of it. It’s a quad core Atom x86 small board computer of the “gutless wonder” variety, and it runs Qubes quite well, just with less performance than the AMD box. However, as I’ve found out in the migration to QubesOS, the amount of computer I actually need for my various uses is a lot less than I’ve historically needed, and a lot less than I assumed I would need when I switched this stuff out. It turns out, the only very intensive things I do anymore are some bulk offline video transcoding, and I have a pile of BOINC compute rigs I can use for that sort of task.
I pretty much run Thunderbird, a few Firefox windows, sometimes Spotify or PlexAmp (which, nicely, run on x86 - that was a problem in my ARM era), a few communications clients, and some terminals. If I have dev projects, I spin up a new AppVM or standalone VM to run them in, and… otherwise, my computers just spend more and more time shut down.
That’s not quite true — apple went out of their way to make the boot secure for third-party OSs as well, according to one of the Asahi devs. So I don’t see them doing any worse than.. basically any other hardware company - those just use hardware components that already have a driver reverse engineered, or in certain cases contributed to some by the producing company, e.g. intel. Besides not having much incentive for opening up the hardware, companies often legally can’t do it due to patents not owned by them, only licensed.
And as for the laptop space, I would argue that the M-series is that good — no other device currently on the market get even in the same ballpark of their performance-efficiency plot to the point I can barely use my non-M laptop as a mobile device.
This is the attitude that I don’t understand. To pick four big chip-makers, I would rank Apple below nVidia, Intel, and AMD; the latter three all have taken explicit steps to ensure that GNU/Linux cleanly boots with basic drivers on their development and production boards. Apple is the odd one out.
On my m1 mac laptop I can work a full 10 hour work day compiling mutliple times without once plugging in my machines. The compiles are significantly faster than other machines and the laptop barely get’s above room temperature.
This is significantly better hardware wise than any other machine I could buy or build on the market right now. It’s not even a competition. Apples hardware is so far ahead of the competition right now that it looks like everyone else is asleep at the wheel.
If you can run your favorite OS on it and get the same benefits why wouldn’t you?
My most recent laptop purchase was around $50 USD. My main workstation is a refurbished model which cost around $150. My Android phone cost $200. For most of my life, Apple products have been firmly out of budget.
That is certainly a fair consideration. But for those who can afford it there are many reasons the price is worth it.
They had to, as servers are predominantly running linux and they are in the business of selling hardware components. Apple is not, so frankly I don’t even get the comparison.
Also, look back a bit earlier and their images are far from stellar, with plenty painstaking reverse engineering done by the Linux community. Also, nvidia is not regarded as a good linux citizen by most people, remember Linus’s middle finger? There has only recently been changes so their video cards could be actually utilized by the kernel through the modern display buffer APIs, instead of having to install a binary blob inside xserver coming with their proprietary driver.
The performance and fanless arguments are icing on the cake and completely moot to me. No previous CPU was ever hindering effectiveness of computing. While I’m glad a bunch of hardware fanatics are impressed by it, the actual end result of what the premium locked down price tag provides is little better in real workload execution. Furthermore they’re not sharing their advancements with greater computing world, they’re hoarding it for themselves. All of which is a big whoop-dee-doo if you’re not entranced by Apple’s first-world computing speeds mindset.
Does Nvidia, Intel or AMD actually “share their advancements with greater computing world”?
AMD definitely does; their biggest contribution is
amd64. Even nVidia contributes a fair amount of high-level research back to the community in the form of GPU gems.If you count GPU gems, I don’t see how apple research is not at least equally valuable.
Which AMD covered in a huge pile of patents. They have cross licensing agreements with Intel and Via (Centaur) that let them have access to the patents, but anyone else who tries to implement x86-64 will hear from AMD’s lawyers. Hardly sharing with the world. The patents have mostly expired on the core bits of x86-64 now, but AMD protects their new ISA extensions.
Didn’t they back off from this at least though? It almost seemed like a semi rogue VP pushed the idea, which was subsequently nixed by likely Tim Cook himself. The emails leaked during that debacle point to a section of the org going off on it’s own.
They did. Eventually. After a year of no communications on the matter beyond “Well, we haven’t shipped it yet.”
I didn’t pay attention to the leaked emails, but it seemed an odd hill to die on for Apple after their “What’s on your phone is your business, not ours, and we’re not going to help the feds with what’s on your device” stance for so long. They went rather out of their way to help make the hardware hard to attack even with full physical access.
Their internal politics are their problem, but when the concept is released as a “This is a fully formed thing we are doing, deal with it,” complete with the cover fire about getting it done over the “screeching voices of the minority” (doing the standard “If you’re not with us, you’re obviously a pedophile!” implications), I had problems with it. Followed by the FAQ and follow on documents that read as though they were the result of a team running on about 3 days of no sleep, frantically trying to respond to the very valid objections raised. And then… crickets for a year.
I actually removed all Apple hardware from my life in response. I had a 2015 MBP that got deprecated, and a 2020 SE that I stopped using in favor of a flip phone (AT&T Flip IV). I ran that for about a year, and discovered, the hard way, that a modern flip phone just is a pile of trash that can’t keep up with modern use. It wouldn’t handle more than a few hundred text messages (total) on the device before crawling, so I had to constantly prune text threads and hope that I didn’t get a lot of volume quickly. The keypad started double and triple pressing after a year, which makes T9 texting very, very difficult. And for reasons I couldn’t work out nor troubleshoot, it stopped bothering to alert me of incoming messages, calls, etc. I’d open it, and it would proceed to chime about the messages that had come in over the past hour or two, and, oh yeah, a missed phone call. But it wouldn’t actually notify me of those when they happened. Kind of a problem for a single function device.
Around iOS 16 coming out, I decided that Lockdown mode was, in fact, what I was looking for in a device, so I switched back to my iOS device, enabled Lockdown, stripped the hell out of everything on it (I have very few apps installed, and nothing on my home screen except a bottom row of Phone, Messages, Element (Matrix client), and Camera), and just use it for personal communications and not much else. The MBP is long since obsolete and gets kept around for a “Oh, I have this one weird legacy thing that needs MacOS…” device, and I’ve no plans to go back to them - even though, as noted earlier, I think the M series chips are the most exciting bits of hardware to come out of the computing world in the last decade or two, and the M series MacBook Pros are literally everything I want in a laptop. Slab sided powerhouses with actual ports. I just no longer trust Apple to do that which they’ve done in the past - they demonstrated that they were willing to burn all their accumulated privacy capital in a glorious bonfire of not implementing an awful idea. Weird as hell. I’ve no idea what I’m going to do when this phone is out of OS support. Landline, maybe.
I followed this basic plan when I went to UNSW to do a co-op on seL4, Concrete Semantics is a really solid textbook although I found myself not really grokking how to navigate between different styles of proof technique when confronted with a massive goal stack in some “real world” proofs I tried to do. Proof Engineering is a lot of fun!
You are so lucky. UNSW is one of the meccas of seL4, and Isabelle in general. I struggle to get proofs any longer than one line most of the time! But yea, it’s surprisingly fun - much like a puzzle.
Curious to know what materials on real proof engineering you went through after Concrete Semantics? I love the book, but have moved to Coq long ago mainly because of the lack of Isabelle-based material that describes practical engineering techniques.
There is https://isabelle.in.tum.de/dist/Isabelle2022/doc/codegen.pdf, which discusses shallow embedding, but Coq has a lot more, e.g. Chlipala’s books.
To an outsider like me, it looks like Emacs development sped up in recent years. LSP and Tree-sitter integrations are especially noteworthy. It’s very impressive.
Piggybacking on this thread: what’s the current state of Emacs when it comes to remote development?
I’m aware of TRAMP but what I’m looking for is more complex.
I’d like a remote machine do most of the work (e.g. compilation, debugging, running a binary, code search). At the same time I’d like the text editing experience to not suffer the network latency so I’d like the client to run locally.
What are my options? Do you have any tried workflows?
It depends a lot on the language you are aiming to work with. Some modes have excellent TRAMP support, and if editing remote files they will fire a remote LSP, compiler / interpreter, etc. Others do not provide TRAMP support at all.
If your favorite major mode does not support TRAMP, one possibility is perhaps to use mosh instead of SSH and run the whole emacs remotely. This can reduce the impact of network latency.
That’s neat, I didn’t know that. I will check it out, thank you!
In my case it’s mostly Rust, Python, Go and sometimes C++.
The python-mode that ships with Emacs works really well with TRAMP, i.e. it fires a remote terminal, etc. I think all popular Python packages, such as anaconda-mode, build on top of it. So you are covered in that front.
I have never tried remote development using the other languages you mentioned.
I don’t think there’s one true easy option for that. Tramp is great but it’s possible individual libraries/modes will have buggy support. Editing over ssh is great if you don’t mind that. Honestly with something like the
kittyterminal using emacs over ssh looks great and works for everything except actual inline images (although kitty can display those on it’s own, but emacs doesn’t know how to tell kitty to draw images… yet).The venerable option of X11 forwarding can work, if latency is low.
Another option that I’ve seen recommended is to basically run emacs gtk with an HTML5 renderer and access via web browser. I haven’t tried it but allegedly there’s a PGTK (pure gtk) branch that has been merged somewhere and since GTK has a method to render to HTML5 you can take advantage of that: https://www.reddit.com/r/emacs/comments/rj8k32/the_pgtk_pure_gtk_branch_was_merged/
Personally I’d just go with either kitty ssh or emacs with remote desktop such as chrome remote desktop or nomachine (as I understand it nomachine is basically a proprietary version of X11 forwarding that’s actually usable for non-trivial applications). I use it every day.
I do this every day for work inside tmux+mosh; mosh does a pretty good job of papering over network latency issues to the point where they’re basically undetectable in my experience. But I’m always connecting to a host in the same city as I’m located so if you want to like … cross an ocean or a continent this may not be viable.
Whereas others responding would run Emacs in SSH, I guess I would run SSH either in Emacs (in
ansi-term-mode) or in a separate terminal emulator alongside Emacs and run the compilation (etc.) commands in the SSH session. If you run those commands with key bindings, I imagine the bindings could be changed to send the commands to the SSH session buffer (if running SSH in Emacs), although I personally have not tried to write programmatically into aterm-modebuffer.I’ve used every 29.1 pretest and rc across Windows, Mac, and Linux (Ubuntu, Debian, Manjaro, and Pop!_OS) and I’ve encountered no majors issues in the last few months. I’ve run these commands more than I’ve ever done before so maybe I will remember them this time lol
sudo apt install build-essential autoconf automake texinfo libgtk-3-dev libxpm-dev libjpeg-dev libgif-dev libtiff-dev libgnutls28-dev libncurses-dev libjansson-dev libgccjit-10-dev ./configure –with-tree-sitter
make -j16
sudo make install
Really happy to see this release. Can’t wait to see all the new modes adopting tree-sitter. Haven’t been this excited about an Emacs release in a while! Looking forward to the day when this is the default Emacs on most Linux Distros but that will take a couple years
Emacs has made incredible progress since the late 2000s. At the time, you had to manage package libraries and versions manually. Plus, there was a lot of glue code you had to copy-paste into ~/.emacs to get it all working. For example, setting up Emacs for Ruby on Rails was quite hard. The outcome was fragile and often broke with updates.
With ELPA and use-package, everything has become much more streamlined, and as a consequence a very rich package ecosystem has emerged. My only complaint right now is that many packages still require a bit of ~/.emacs code to get up and running. Plus, documentation about how to mix and match packages to get IDE-like features is not great. The best source for that is, paradoxically, Doom Emacs. IMHO, this scares beginners away compared to VS Code, which is a shame.
I still remember the day when I read Your Text Editor Is Malware, I removed all the Emacs packages and manually git cloned or copy-pasted them to get some illusion of safety.
I guess the primary benefit by not using a package manager is getting a better understanding of their dependencies.
I tried the build instructions here and they didn’t work on Debian 12. Just FYI, you need to use
libgccjit-12-devinstead oflibgccjit-10-dev.The point being that you probably shouldn’t blindly copy this in the hopes it will work.
Resigning! I just submitted my resignation, so have started my notice period at Microsoft. Looking forward to starting the new thing after it ends.
Good luck at your new post. Will you continue to work on CHERI?
Yup. My new employer aims to ship CHERIoT products (Microsoft wants to use it in some places but not where users can see it). I’ll share more details in October. I’ll be hiring probably around December.