It's interesting btw that Martin Kleppmann lists a couple of proof assistants, but not model checkers like TLA+. With him working extensively on distributed systems, I would have thought that would be on the list as well.
It appears many of the proof assistants/verification systems can generate OCaml. Or perhaps ADA/Spark?
Regardless of how the software engineering discipline will change in the age of gen AI, we must aim to produce higher not lower quality software than whatever we have today, and formal verification will definitely help.
The main designer is Andreas Rumpf, but investigating the git commits of the new Nim reveals more people being involved. [1] Whether Andreas is a genius, I have no idea, but he has been doing compiler and language development for over 20 years [2] so he's probably extremely knowledgeable regardless.
It is an excellent book and one of the canonical texts on the subject. My only suggestion for the "Lox" language would be to include an implementation of arrays, and preferably also hash/dict arrays. Other than that, the book contains everything you need to know about implementing a programming language.
It's hard to say what "that hard" should be considered, but the book's first half involves Java reflection, which isn't obvious code to port to different languages in my opinion.
Does it? I know it uses metaprogramming (a Java program that outputs another Java program), but that’s probably easier in other languages than in Java. In my Python implementation I was able to significantly simplify that part of the code by using `eval`.
I do remember him using the visitor pattern to implement part of the parser I think. I thought that was kind of an odd choice, especially since it seemed like he was really just trying to avoid Java boilerplate.
Regardless, the book is incredible, and the choice of Java to start with makes sense. Its probably going to be the most universally approachable for everyone, even if they aren't super familiar. C can be pretty overwhelming if you aren't familiar it.
> I do remember him using the visitor pattern to implement part of the parser I think. I thought that was kind of an odd choice, especially since it seemed like he was really just trying to avoid Java boilerplate.
It's used to allow writing a "resolver" and an "interpreter" that both know how to handle every type of node in the AST. It's almost a functional approach, and I actually think it might increase boilerplate because Java is more designed around the object-oriented approach of adding `resolve` and `interpret` methods directly to each node type.
The two approaches result in very different code organisation, though - maybe the visitor approach was easier to explain in prose.
It's been a while since I read it, but I remember him saying something about the more natural (my word not his) approach being a single data structure that you would pass through both components, but he didn't want to do that because Java doesnt really encourage that kind of design, and you have a bunch of boilerplate for each class. It just struck me as an odd choice since the book was more about compiler/interpreter fundamentals, and I feel like the visitor pattern is a bit in the weeds in terms of OOP design.
I wonder if he wrote today if he would have used a Record and done the more straightforward implementation.
I went through the Crafting Interpreters book with modern Java. I posted this on reddit, but I basically used records and sealed interfaces. With modern Java there's no need for visitor pattern.
private void execute(Stmt statement) {
switch (statement) {
case Stmt.Expression expression -> evaluate(expression.expr());
case Stmt.Block block -> executeBlock(block.statements(),
new Environment(environment));
...
public sealed interface Expr permits
Expr.Assign,
Expr.Binary,
Expr.Call,
Expr.Function,
.... more exprs here
Interesting. Almost all my actual experience writing Java is in Java 8, so I'm not super familiar with the modern stuff (other then a few things like Records). I'll have to take a look.
Most of the people I know who write Java would have an aneurysm at seeing a switch statement.
To be clear, that's a critique of the Java mindset, not your code. Lol
It's been a few years now, but there's no real reason to port the Java code directly – you can just read what it's trying to do, and implement that using your language's idioms. I don't remember anything as complex as trying to port reflection.
I understand. I wasn't a Java person when I read that book, yet I still prefer Java over more esoteric options. If Golang is easier for you to understand (no OOP), then I can recommend this one:
Wren, the topic of the post, is positioned as a descendant of Smalltalk, the most OOP language of them all. The author clearly finds the OOP paradigm important.
This is awesome. Thank you for sharing. I have been working on a small interpreted language for shell scripts with lots of help from Claude Code. The main idea is to automatically generate the cli interface for the scripts based on function definitions. However, I'm far from a programming languages expert, so I've been a bit hesitant to share my work. Going to give this book a read this week to see how far I am. Thank you!
Yeah, my understanding is that the bytecode interpreter in the second half of the book is essentially a stripped-down version of the Wren virtual machine.
...If you're using the alloc/std crates (which to be fair, is probably the vast majority of Rust devs). libcore and the Rust language itself do not allocate at all, so if you use appropriate crates and/or build on top of libcore yourself you too can have an explicit-allocation Rust (though perhaps not as ergonomic as Zig makes it).
I think zig generally composes better than rust. With rust you pretty much have to start over if you want reusable / composable code, that is not use the default std. Rust has small crates for every little thing because it doesn't compose well, as well to improve compile times. libc in the default std also is major L.
It mainly comes down how the std is designed. Zig has many good building blocks like allocators, and how every function that allocates something takes one. This allows you to reuse the same code for different kind of situations.
Hash maps in zig std are another great example, where you can use adapter to completely change how the data is stored and accessed while keeping the same API [1]. For example to have map with limited memory bound that automatically truncates itself, in rust you need to either write completely new data structure for this or rely on someone's crate again (indexmap).
Errors in zig compose also better, in rust I find error handling really annoying. Anyhow makes it better for application development but you shouldn't use it if writing libraries.
When writing zig I always feel like I can reuse pieces of existing code by combining the building blocks at hand (including freestanding targets!). While in rust I always feel like you need go for the fully tailored solution with its own gotchas, which is ironic considering how many crates there are and how many crates projects depend on vs. typical zig projects that often don't depend on lots of stuff.
> Nearly all systems have the ability to call libraries written in C. This is not true of other implementation languages.
From section "1.2 Compatibility". How easy is it to embed a library written in Zig in, say, a small embedded system where you may not be using Zig for the rest of the work?
Also, since you're the submitter, why did you change the title? It's just "Why is SQLite Coded in C", you added the "and not Rust" part.
The article allocates the last section to explaining why Rust is not a good fit (yet) so I wanted the title to cover that part of the conversation since I believe it is meaningful. It illustrates the tradeoffs in software engineering.
It's interesting to observe how many people are undergoing an identity crisis due to the emergence of LLMs challenging the status quo.
What will our craft of programming turn into? So far programming has been quite fun and creative, but LLMs are undeniably changing the programmer's game. Will it still be as enjoyable? I don't know. But then, what else could we switch to which would allow us to be highly creative while still maintaining control?
Perhaps this is similar to how people felt during the industrial revolution.
A better term would be “Augmented Engineering” (AE).
You want something to inspire engineers to do their best work.
When you can expand your capabilities using the power of AI, then yeah, you can do your best work; hence augmented engineering.
But vibing? Not so much.
I guess AE could also stand for Advanced Engineering, after all the AI gives you the power to access and understand the latest in engineering knowledge, on demand, which you can then apply to your work.
I wouldn't worry too much about what to call it. Assigning a distinct label separates it from traditional engineering in a way that it assumes AI-assisted coding is only for a subset of developers. At some point the unusual approach will be writing code without any AI assistance. So the transition will leave the "vibe" behind.
> gives you the power to access and understand the latest in engineering knowledge, on demand, which you can then apply to your work.
Gives you access to the power to access and {mis}understand the {most repaeted over the last 1-10 years} engineering {errors, myths, misunderstandings, design flaws}, on demand, which you then can apply to your work {to further bias the dataset for future models to perpetuate the slop}.
Do NOT trust AI agents. Check their work at every level, find any source they claim to use, and check its sources to ensure that itself isn't AI too. They lie beyond their datasets, and their datasets are lying more for every minute that pass.
Now, seriously though, no tools is perfect, and I agree we should not trust it blindly, but leaving aside AI Agents, LLMs are very helpful in illuminating one's path, by consulting a large body of knowledge on demand, particularly when dealing with problems which might be new to you, but which have already been tackled one way or another by other people in the industry (provided they're in the training set of course).
Yes, there's always the risk of perpetuating existing slop. But that is the risk in any human endeavor. The majority of people mostly follow practices and knowledge established by the few. How many invent new things?
To be honest, I haven't yet used AI agents, I'm mostly just using LLMs as a dialogue partner to further my own understanding and to deepen my knowledge. I think we're all still trying to figure it out how to best use it.
> A better term would be “Augmented Engineering” (AE).
I don't think it necessarily deserves a special name. It is just engineering. You don't say book assisted engineering when you use a book as a reference. It is just engineering.
> But vibing? Not so much.
Just call it yolo engineering. Or machine outsourced irresponsible lmao engineering.
> I guess AE could also stand for Advanced Engineering, after all the AI gives you the power to access and understand the latest in engineering knowledge, on demand, which you can then apply to your work.
I know quite some people in the safety/aviation domain that kind of dislike the subranges, as it inserts run-time checks that are not easily traceable to source code, thus escaping the trifecta of requirements/tests/source-code (which all must be traceable/covered by each other).
Weirdly, when going through the higher assurance levels in aviation, defensive programming becomes more costly, because it complicates the satisfaction of assurance objectives. SQLite (whiches test suite reaches MC/DC coverage which is the most rigorous coverage criterion asked in aviation) has a nice paragraph on the friction between MC/DC and defensive programming:
Ideally, a compiler can statically prove that values stay within the range; it's no different than proving that values of an enumeration type are valid. The only places where a check is needed are conversions from other types, which are explicit and traceable.
let a: u8 is 0..100 = 1;
let b: u8 is 0..100 = 2;
let c = a + b;
The type of c could be u8 in 0..200. If you have holes in the middle, same applies. Which means that if you want to make c u8 between 0..100 you'd have to explicitly clamp/convert/request that, which would have to be a runtime check.
In your example we have enough information to know that the addition is safe. In SPARK, if that were a function with a and b as arguments, for instance, and you don't know what's being passed in you make it a pre-condition. Then it moves the burden of proof to the caller to ensure that the call is safe.
But obviously the result of a + b is [0..200], so an explicit cast, or an assertion, or a call to clamp() is needed if we want to put it back into a [0..100].
Comptime constant expression evaluation, as in your example, may suffice for the compiler to be able to prove that the result lies in the bounds of the type.
That's pohibitively expensive in the general case when external input is used and/or when arithmetic is used on the values (main differerence to sum-types).
The branch of mathematics you need to compute the bounds of the result of an operation is called Interval Arithmetic [1]. I'm not sure of where its limits are (hah), but at the very least it provides a way to know that [0,2] / [2,4] must be within [0,1].
I see there's some hits for it on libs.rs, but I don't know how ergonomic they are.
This is basically excuses being made by C people for use of a language that wasn't designed for and isn't suitable for safety critical software. "We didn't even need that feature!"
Ada's compile time verification is very good. With SPARK it's even better.
Runtime constraints are removable via Pragma so there's no tradeoff at all with having it in the language. One Pragma turns them into static analysis annotations that have no runtime consequences.
> as it inserts run-time checks that are not easily traceable to source code
Modifying a compiler to emit a message at every point that a runtime check is auto-inserted should be pretty simple. If this was really that much of an issue it would have been addressed by now.
To elaborate on siblings compile time vs run time answer: if it fails at compile time you'll know it's a problem, and then have the choice to not enforce that check there.
If it fails at run time, it could be the reason you get paged at 1am because everything's broken.
It’s not just about safety, it’s also about speed. For many applications, having to check the values during runtime constantly is a bottleneck they do not want.
Like other sibling replies said, subranges (or more generally "Refinement types") are more about compile-time guarantees. Your example provides a good example of a potential footgun: a post-validation operation might unknowingly violate an invariant.
It's a good example for the "Parse, don't validate" article (https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...). Instead of creating a function that accepts `int` and returns `int` or throws an exception, create a new type that enforces "`int` less than equal 200"
class LEQ200 { ... }
LEQ200 validate(int age) throws Exception {
if (age <= 200) return age;
else throw Exception();
}
LEQ200 works = validate(200);
// LEQ200 fails = validate(201);
// LEQ200 hmmm = works + 1; // Error in Java
LEQ hmmm = works.add(1); // Throws an exception or use Haskell's Either-type / Rust's Result-type
Something like this is possible to simulate with Java's classes, but it's certainly not ergonomic and very much unconventional. This is beneficial if you're trying to create a lot of compile-time guarantees, reducing the risk of doing something like `hmmm = works + 1;`.
These kind of compile-time type voodoo requires a different mindset compared to cargo-cult Java OOP. Whether something like this is ergonomic or performance-friendly depends on the language's support itself.
Your example also gets evaluated at comptime. For more complex cases I wouldn't be able to tell you, I'm not the compiler :) For example, this get's checked:
let ageFails = (200 + 2).Age
Error: 202 can't be converted to Age
If it cannot statically prove it at comptime, it will crash at runtime during the type conversion operation, e.g.:
import std/strutils
stdout.write("What's your age: ")
let age = stdin.readLine().parseInt().Age
Then, when you run it:
$ nim r main.nim
What's your age: 999
Error: unhandled exception: value out of range: 999 notin 0 .. 200 [RangeDefect]
Exactly this. Fails at runtime. Consider rather a different example: say the programmer thought the age were constrained to 110 years. Now, as soon as a person is aged 111, the program crashes. Stupid mistake by a programmer assumption turns into a program crash.
Why would you want this?
I mean, we've recently discussed on HN how most sorting algorithms have a bug for using ints to index into arrays when they should be using (at least) size_t. Yet, for most cases, it's ok, because you only hit the limit rarely. Why would you want to further constrain the field, would it not just be the source of additional bugs?
Once the program is operating outside of the bounds of the programmers assumption, it’s in an undefined state that may cause a crash to happen at a later point of time in a totally different place.
Making the crash happen at the same time and space as the error means you don’t have to trace a later crash back to the root cause.
This makes your system much easier to debug at the expense of causing some crashes that other systems might not have. A worthy trade off in the right context.
Out of bounds exception is ok to crash the program. User input error is not ok to crash the program.
I could go into many more examples but I hope I am understood. I think these hard-coded definition of ranges at compile time are causes of far more issues than they solve.
Let's take a completely different example: size of a field in a database for a surname. How much is enough? Turns out 128 varchars is not enough, so now they've set it to 2048 (not a project I work(ed) on, but am familiar with). Guess what? Not in our data set, but theoretically, even that is not enough.
> Out of bounds exception is ok to crash the program. User input error is not ok to crash the program.
So you validate user input, we've known how to do that for decades. This is a non-issue. You won't crash the program if you require temperatures to be between 0 and 1000 K and a user puts in 1001, you'll reject the user input.
If that user input crashes your program, you're not a very good programmer, or it's a very early prototype.
I think, if I am following things correctly, you will find that there's a limit to the "validate user input" argument - especially when you think of scenarios where multiple pieces of user input are gathered together and then have mathematical operations applied to them.
eg. If the constraint is 0..200, and the user inputs one value that is being multiplied by our constant, it's trivial to ensure the user input is less than the range maximum divided by our constant.
However, if we are having to multiply by a second, third... and so on.. piece of user input, we get to the position where we have to divide our currently held value by a piece of user input, check that the next piece of user input isn't higher, and then work from there (this assumes that the division hasn't caused an exception, which we will need to ensure doesn't happen.. eg if we have a divide by zero going on)
I mean, yeah. If you do bad math you'll get bad results and potentially crashes. I was responding to someone who was nonsensically ignoring that we validate user input rather than blindly putting it into a variable. Your comment seems like a non sequitur in this discussion. It's not like the risk you describe is unique to range constrained integer types, which is what was being discussed. It can happen with i32 and i64, too, if you write bad code.
Hmm, I was really pointing at the fact that once you get past a couple of pieces of user input, all the validation in the world isn't going to save you from the range constraints.
Assuming you want a good faith conversation, then the idea that there's bad math involved seems a bit ludicrous
I believe that the solution here is to make crashes "safe" eg with a supervisor process that should either never crash or be resumed quickly and child processes that handle operations like user inputs.
This together with the fact that the main benefit of range types is on the consumption side (ie knowing that a PositiveInt is not 0) and it is doable to use try-catch or an equivalent operation at creation time
For some reason your reply (which I think is quite good) makes me think of the adage "Be liberal in what you accept, and conservative in what you send" (Postels law).
Speaking as someone that's drunk the Go kool aid - the (general) advice is not to panic when it's a user input problem, only when it's a programmers problem (which I think is a restatement of your post)
Happens with DB constraints all the time, user gets an error and at least his session, if not whole process, crashes. And yes that too is considered bad code that needs fixing.
> Stupid mistake by a programmer assumption turns into a program crash.
I guess you can just catch the exception in Ada? In Rust you might instead manually check the age validity and return Err if it's out of range. Then you need to handle the Err. It's the same thing in the end.
> Why would you want to further constrain the field
You would only do that if it's a hard requirement (this is the problem with contrived examples, they make no sense). And in that case you would also have to implement some checks in Rust.
Also, I would be very interested to learn the case for hard requirement for a range.
In almost all the cases I have seen it eventually breaks out of confinement. So, it has to be handled sensibly. And, again, in my experience, if it's built into constraints, it invarianly is not handled properly.
Consider the size of the time step in a numerical integrator of some chemical reaction equation, if it gets too big the prediction will be wrong and your chemical plant could explode.
So too big times steps cannot be used, but constant sized steps is wasteful. Seems good to know the integrator can never quietly be wrong, even if you have to pay the price that tge integrator could crash.
Exactly, but how do you catch the exception? One exception catch to catch them all, or do you have to distinguish the types?
And yes... error handle on the input and you'd be fine. How would you write code that is cognizant enough to catch outofrange for every +1 done on the field? Seriously, the production code then devolves into copying the value into something else, where operations don't cause unexpected exceptions. Which is a workaround for a silly restriction that should not reside in runtime level.
If you're using SPARK, it'll catch at compile time if there's ever a possibility that it would fit within that condition. Otherwise it'll throw an exception (constraint_error) during runtime for you to catch.
No, range types are at best a very limited piece of DbC. Design by Contract lets you state much more interesting things about your program. It's also available in Ada, though.
IM[EO], the std library and system interfaces are complete obscure made-up trash. The language was fine and tooling is nice, but I decided I'll neveer try to use nim again.
The second story, and highly upvoted, on HN right now is: "AI will make formal verification go mainstream"[1].
[1] https://news.ycombinator.com/item?id=46294574