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.
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.
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).
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.
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]
Hmm, I guess this then makes sense if we regard the app as a latent space projecting user's data, so its views are awaiting to be activated.
Seen this way, the app is basically communicating to the user: Hey I have "Your Pictures", "Your Cases", etc. Click to find out.
But to me the "My ..." variation also makes sense. e.g. In Photos app on macOS you will see "My Albums", "My Projects", and although they can be renamed, I don't think I created them.
But for UI elements? Should I name say a tab “My Pictures” and not “Your Pictures” because clicking on said tab I’m communicating to the system I want to see my pictures?
Looking at some YouTube videos, it looks like this was the greeting upon booting:
“Stored on this single, 1.44 Mbyte floppy disk is a demo copy of the QNX realtime operating system, the Photon microGUI windowing system, the Voyager web browser, Ethernet networking, TCP/IP, an embedded web server, an editor, a file browser, a vector graphics animation, and a television set-top box simulation.
Just think — if we can do all this with a 1.44 Mbyte floppy disk, imagine the devices you could build with QNX realtime technology.”
We used to infer one’s mind from their writing. Nowadays?
I’m surprised people are too lazy to even remove them dashes.
Well, in fact it might actually be a good thing for one can spot when something was AI generated much easier.
I feel like original writing is pretty much dead these days. We’re all best selling authors now.
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