This Scott Wlaschin talk [1] is a good introduction to TLA+. And the slides [2].
[1] https://www.youtube.com/watch?v=qs_mmezrOWs
[2] https://speakerdeck.com/swlaschin/tla-plus-for-programmers
Readit NewsplainOldText commented on AI will make formal verification go mainstream martin.kleppmann.com/2025... · Posted by u/evakhoury
I guess it’s time to learn OCaml then.
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.
plainOldText commented on NJVL: Nim's New Intermediate Representation github.com/nim-lang/nimon... · Posted by u/generichuman
Nim seems to be almost a pet project of a single individual. Is that just my interpretation or is it an actual representation of reality?
If it is correct, and mostly created by one person - how? Are they a genius? Is creating your own programming language from scratch something anyone can accomplish if they just go for it?
Or is it just something that shouldn't be trusted/used for commercial purposes because it's not as "legit" as a newer language like rust for example?
It's just a weird vibe - it seems like it should be so much more popular than it is.
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.
[1] https://github.com/nim-lang/nimony/commits/master/
[2] https://en.wikipedia.org/wiki/Nim_(programming_language)
plainOldText commented on Wren: A classy little scripting language wren.io/... · Posted by u/Lyngbakr
Reminder the creator of Wren wrote the awesome Crafting Interpreters book [0].
plainOldText commented on Why Is SQLite Coded In C sqlite.org/whyc.html... · Posted by u/plainOldText
> 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.
plainOldText commented on Why Is SQLite Coded In C sqlite.org/whyc.html... · Posted by u/plainOldText
I’d be curious to know what the creators of SQLite would have to say about Zig.
Zig gives the programmer more control than Rust. I think this is one of the reasons why TigerBeetle is written in Zig.
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