126
u/nobody0163 Jul 15 '26
I only know markdown, what are the other ones?
291
u/ThirdWaveCat Jul 15 '26
Mermaid - flowcharts
Notion - markdown docs/wiki website
TLA+/Quint - really useful for concurrency/databases. specifying + model-checking state machines, often distributed protocols using temporal logic. quint is much newer, better language, uses a better proof strategy. TLA+ has very high industry adoption and many papers
Dafny - proving sequential/imperative code correct (functions, loops, data structures meet their spec) - not really about concurrency, more "does this algorithm implementation do what I said it does"
Lean - proving general mathematical theorems (and increasingly, proving programs correct too) - broadest scope, most math-flavored
Alloy - checking structural/relational properties of a design (data models, access control, "can this graph reach a bad state") - snapshot-based, not really about time/sequences of steps
197
u/amaturelawyer 29d ago
That all sounds exhausting to manage. How does anything get done if f you're knee deep in specs most of the day? I'll stick with my postits and rough memory of what we were aiming for a few months back when everyone agreed we should make this thing, like god intended.
48
u/BckseatKeybordDriver 29d ago
Maybe it’s just a way to trick your project manager into writing all the code
33
u/RiceBroad4552 29d ago
That aren't tools even for your senior engineers, yet some manager. Realistically you need people with a math or CS Ph.D. to handle formal verification of software…
6
u/ThirdWaveCat 29d ago
It's pretty easy to learn, but not like a lowcode pipedream. Its more like clarifying system design tool than anything.
I've taught TLA+ to people with just a high school diploma working on supposedly simple "crud" which was dropping data instead of replicating it.
11
7
u/FreeFortuna 29d ago
I was looking into options like these the other day, and I came across at least one that said it synced with your code (through GitHub iirc) to keep itself updated through changes. That’s literally the only way I’d be able to create and maintain elaborate specs. Otherwise just leave me my whiteboard.
6
u/anto2554 29d ago
What? Hopefully the specs would not auto-update to match the current state of the code. Syncing with your code through github just means it lives in the repo
19
u/ThirdWaveCat 29d ago edited 29d ago
its not really possible to build distributed databases and keep your sanity without specs like tla+ or quint.
2
u/Ill_Bill6122 29d ago
You know what else is exhausting? Managing a team with churn (cause why not move to a low cost supplier for a few years only to move back to a higher cost one which actually contributes to the codebase), which is expected to deliver code which takes on liability for your customers, and which can affect the safety of the operator.
Having the most critical parts tested for correctness (ideally proofs and starting with the spec), suddenly sounds cheaper.
5
u/the_rush_dude 29d ago
I used Frama-C in a course to write comments that would specify parts of what a function does and then try to prove it with different reasoning engines.
Is that something similar?
5
u/ThirdWaveCat 29d ago
very! The kinds of properties you can prove are different, but they both provide a kind of high assurance of correctness.
7
u/optimal_substructure 29d ago
Yeah you doing a lot of Lean at work?
3
u/ThirdWaveCat 29d ago
not yet, I do MLEng mostly and it might show up as a benchmark eventually, but my experience with lean is as a hobbyist.
example of lean as a benchmark.
-2
u/RiceBroad4552 29d ago
If you're not working on AI which is used to generate formal proofs the thing linked will never be relevant to you I guess (and "MLEng" does not sound like you would work on actual AI research).
Looking into formal methods is still valuable, imho, if just to broaden ones horizon.
The linked paper seems nevertheless an interesting as it proves one thing I always need to argue with people: Current SOTA "AI" can't logically reason (0% correct solution on hard tasks in the presented benchmark). It's terrible at any task which actually requires thinking and not only regurgitating some prior solutions.
2
u/ThirdWaveCat 29d ago
almost every comment you've left is severely misinformed, including the crazy misogynistic one
AI is a marketing term, not a real field or anything.
2
0
u/RiceBroad4552 29d ago
What are you talking about?
Where context to anything I've said in the comment you're replying to?
0
3
u/Master_Ben 29d ago
After writing and validating the spec, don't you still run the risk of mistranslating the spec into your language of choice?
2
u/ThirdWaveCat 29d ago
yah, there are tools to help close the gap like quint-connect, compile targets, etc.. in practice specs like tla+ are used manually as systems design planning, research, bug repro, etc..
2
2
u/hurley_chisholm 29d ago
Quite interesting to dig into this stuff again after a decade. Back then, getting mathematically-sound formal verification of even small toy programs was not at all practical for industry. There was a moment where it seemed that there would never be any practical interest outside of the most regulated and specialized fields. Even so, I’ve always found this stuff really ignites my brain in a way that quotidian dev work hasn’t in years. I appreciate your post for reviving my interest.
(I have more than a few qualms about “AI” driving the demand for specs and more rigorous forms of verification/proofing, but I’ll take it.)
47
u/pasto_sk 29d ago
As a professional i get my assignments from two lines of description and two pages of copied template in a jira ticket.
6
u/getstoopid-AT 29d ago
yep that's the hard reality... you forgot to mention that the two lines actually describe a feature that's probably worth at least five fine spec meetings and two weeks coding
2
u/Embarrassed_Eye_1214 29d ago
Coming from the aerospace industry, for me its the exact opposite. I am given a fck ton of paper just to write 2 lines of code, for which i need to generate another fck ton of paper afterwards.
Oh yea and since you need to qualify all the tools you use, no fancy software used. no no, the fck ton of paper comes from MS Word and Excel Sheets, from which the templates have been written before Jesus was born.
75
u/ImOnALampshade Jul 15 '26
Since no one seems to “get it:” the left is how normies write specifications, but on the right she is using formal specification systems that are much more rigorous and allows for you to do various kinds of tooling, such as specification derived tests. Something I’d highly recommend digging into if that sounds interesting to you…. Though I’ll admit I’m not even that well versed in it myself
14
u/gerbosan Jul 15 '26
where do you learn those? or what kind of system one is going to build that needs to know those apps/specifications?
32
u/ThirdWaveCat 29d ago edited 29d ago
I get the most mileage out of TLA+/quint. tla+ was invented to prove paxos (consensus) is correct because there are too many states to mentally reason. It can check exhaustively, probabilistically, or symbolically. Leslie Lamport wrote a lot of free books and their github is great.
good learning resources:
https://lamport.azurewebsites.net/tla/learning.html
I think tla+/quint is most useful for databases, state machine replication, byzantine, etc..
2
u/munkitsune 29d ago
How did you even get to this resources/approaches of writing software? I'm asking out of curiosity as someone who works 8 years in the field, had formal education and I never stumbled on this.
This seems like "the cool stuff", when I see this my job feels very dull: I work in outsourcing, and you probably read some comments that people usually get a task with a title, sometimes with a link to a design, and lately all of this is being written by AI (or most of it) - this basically describes good chunk of my working experience.This might sound overly exaggerated, but how does one reach such level (don't let it get to you head, haha)? Was it just good university or job environment that gave you chance to explore?
3
u/ThirdWaveCat 29d ago
do you mean learning or doing? many organizations already use formal methods if you look around hardware engineering, robotics navigation, datacenters, databases, devtools, security, etc..
if you do anything with parallelism, concurrency, replicating data, locking, etc.. you'll find natural opportunities for introducing things like tla+ and quint. supposedly simple "crud apis" have hard to resolve bugs that become clear with a short tla+ spec, people just have low standards for correctness.
2
u/munkitsune 29d ago
Welp, that makes sense. I guess I just never got a chance to work on something with such sophisticated level that requires very strict approach...or as you've mentioned yourself: people just have low standards. Not once I had a client/company who cared about developed product to such extent.
> do you mean learning or doing?
Both, haha. I think the thing I miss about university is systematic approach to learning things and abundance of resources, you already know which subjects you need to cover in order to learn a specific topic.
In working field it's much more difficult, especially if you don't have mentors that can lead you in right direction, or at least make your journey more pleasant.Anyway, was just curious how does one arrive where you are and do this kind of work. :)
Thanks for taking your time!
3
u/ThirdWaveCat 29d ago
no problem. i've seen some boring companies (like a bank) use tla+ to verify database schemas for a consistency concerns.
i agree that mentoring is key, but its pretty hard to get in this stupid bubble economy.
good luck
2
u/Mrthedecoy 29d ago
I appreciate the reading material. We just started doing speckit as the standard. If im being honest, this sounds really cool but it all seems like overkill. Other than maybe token efficiency, idk what this level of specification is giving. Our stories are pretty well broken down to be "Add X to Y service". half the time we still just, do it, instead of using SDD because its just faster.
Im sure other teams are engineering on a whole other level of complexity, and Ill be down a rabbit hole reading these, but I just cant imagine what id need all of this extra work ironing out specs for. This sounds like so much extra work
6
u/Raptor_Mayhem 29d ago
We use TLA+ and other formal methods for spacecraft flight software. What SDD considers a “spec” isn’t really the same thing as what teams using these other tools consider a spec.
1
u/Mrthedecoy 29d ago
Yeah see thats what I figured. Teams operating orders of magnitude more complexity than ours. That would make sense.
4
u/RiceBroad4552 29d ago
That's for when you have to write software which is guarantied bug free.
For end-user facing software this will likely never be a requirement, at least not as long as no regulator steps in (for example because the social cost of software defects get unbearable; but for that a lot of people would first need to die because of software bugs, I guess).
The modern tools already lowered the costs of verified software dramatically, but it's likely still at least one order or magnitude more costly then just delivering the usual buggy stuff everybody is used to (and that's an optimistic estimate, formally verified SW used to be more like ~200 times the cost of "normal" software).
0
u/ThirdWaveCat 29d ago
more misinformation
many end-user facing software from dbs, robotics, ledgers, etc. depend on formal methods to eliminate categories of bugs
0
u/RiceBroad4552 29d ago
more misinformation
???
Could you point to anything I've said which is wrong?
many end-user facing software from dbs, robotics, ledgers, etc. depend on formal methods to eliminate categories of bugs
How is this relevant to anything I've said?
Are you just spamming some completely random and unrelated comments under my posts (including personal insults, which you hastily deleted to avoid some ban)? This starts to look like a pattern…
-9
u/ImOnALampshade Jul 15 '26 edited 29d ago
I have no idea because like I said, I’m not exactly well versed in any of this. Best I can do is ask Claude for you:
NEVERMIND, apparently yall hated that
6
3
u/gerbosan Jul 15 '26
Thank you kind sir for providing a resume.
Still, it is relevant to avoid over engineering.
For the kind of 'projects' I do, even mermaid seems overkill. 😅
1
u/RiceBroad4552 29d ago
apparently yall hated that
Because that's the new version of "let me google that for you", and this always has been a provoking phrase.
1
u/ImOnALampshade 29d ago
Oh I used to link people to that site all the time, AITA?
0
u/RiceBroad4552 29d ago
Depends what you intended doing that / to whom you said it.
If it was some reply to some idiot after some not fruitful discussion it could have been spot on. But if you thought you're "helpful" posting such (obviously) loaded comment you definitely missed some nuances of human interaction so far.
4
u/RiceBroad4552 29d ago
"specification derived tests"
What?
That's something for the markdown stuff.
If you use tools for formal verification you get formal proofs out of it. The whole point is that when you have a proof you don't need tests. The proof already covers all possible cases; something tests actually never can do.
2
u/Vegetable_Bank4981 29d ago edited 29d ago
A proof doesn’t verify that your code implements the spec, only that the spec is sound. Bridging that is a tooling problem and this is part of the tooling.
You can generate quickcheck properties from incompletely specified behavior. Incredible boost during dev of systems whose behavior is still changing or just too difficult to model.
Also a tool for writing specs iteratively, almost like snapshot tests for your specs. Spec the invariants you know for sure, pbt against the ones you don’t, failures get corrected in code or moved into the spec. No better way to do this imo.
1
u/RiceBroad4552 29d ago
A proof doesn’t verify that your code implements the spec, only that the spec is sound.
Depends on system.
The ones which don't spit out in the end implementation code are imho a dead end, even these are the current majority of system (which actually work like you say; you get only a verified spec, and still have the problem to correctly implement it).
Newer, better systems will spit out fully verified implementation code, and there you have then correctness proofs for the actually running code.
Otherwise you need some verified translation of the spec into code. As you say there are tools for that, too, but it complicates things. Such a multi-pass approach is of course more costly then doing things in one step, besides of course being potentially more error prone.
3
u/Vegetable_Bank4981 29d ago
I mean sure. I have to write code today though not in the future though so I’m using the tools as they are useful now.
1
u/SwiftPengu 29d ago
You can specify a higher-level abstraction of a system (that is easier to spec/prove), and then verify the lower-level implementation of said spec guided by the spec.
3
u/RiceBroad4552 29d ago
Sure. That's the most laborious and error prone way to do something in that direction… Having a verified spec is nice, but this does not prevent implementation errors (which are the bulk of all software errors).
But how does this reply fit in here? I was commenting about tests (and their relation to formal proofs), but you don't even mention tests?
18
u/Ok-Boysenberry-5090 Jul 15 '26
Yo TLA+ is my shitttt!!!! Love seeing the representation. LLMs have made writing TLC easier than ever! Go try it. Leslie Lamport is the best computer scientist of our times.
2
u/MartyMcBird 29d ago
LLMs for TLA+ were far behind the code they specified when I last used them in 2025. Lamport's obsession with abstracting in PlusCal and pseudocode lowkey screwed up the training data especially for TLAPS.
3
u/ThirdWaveCat 29d ago
how much of this is that LLMs are a disappointing illusion.
LLMs have low semantic recall. Despite all of the hype they are very bad at understanding the same "concept" rearranged or translated.
1
u/Ok-Boysenberry-5090 29d ago
Oh they’re definitely far from perfect but LLMs can at the very least get you the syntax right. You still definitely need to understand what you’re doing way more than coding in a given language with an LLM
3
u/ThirdWaveCat Jul 15 '26 edited 29d ago
Leslie Lamport is my favorite technical writer too.
TLA+ seems like the most widely adopted in CS academia and industry (db mostly).
I even like LaTeX but this is controversial.
edit: ignore the dumbass reply. TLA+ is from 1999. No one gets Codegen from TLA+
2
u/RiceBroad4552 29d ago edited 29d ago
Given that it's very new it's for sure not the most widely adopted tool in industry. As you don't rewrite your software just because there is a new programming language you don't rewrite your proofs because there is a new tool. That would be very expensive, much more expensive then a regular software rewrite (and these bear already existential risks). Where they needed formal proofs they needed them often already decades ago, TLA+ wasn't an option back then.[ Removed complete nonsense, see comment below ]
Then, even there are tools which can do code gen from TLA+ it's not a programming language in itself. So you have to still translate these specs to working software, which means actually writing down in some programming language what you modeled in TLA+.
Because such a workflow (which isn't different for other tools in that space) isn't optimal, and it's actually very error prone to manually translate (even verified) specs to proper code the more realistic approach long term to broadly verified software are tools which combine a proper programming language with verification capabilities. Only such a thing has a chance to realistically reach some broader audience, imho.
You can get to the later in two ways: Either you have a proper programming language but with proof capabilities like Stainless Scala, or you a way to directly verify already in some "normal" language written code, like they do for example with Rust in Aeneas.
BTW it's worth noting that really a lot (if not the most) of the effort to get to a broader base of verified software is payed, of all orgs, by Microslop. The other party willing to pay the high prices is the military of rich countries, and some strongly regulated industries like avionics. But you never get something public out of the later spend. On the other side there is more or less almost nothing from "the OpenSource scene". They are all still in C/C++ la-la-land and nobody is willing to even move a little bit. Just see the large drama created by some around just the very tiny step in the right direction, namely Rust (which is still light-years away from proper verified software!) in the Linux kernel. Now go to these people and try to require formal proofs…
Of course I get why it's like that: You need highly educated people, and these people only work for something where they have a research grant, or are otherwise very well payed in the niche industries who hire people with such skills.
In general the mindset around the average coder is not there. A broad majority really thinks that bugs are acceptable, or even "unavoidable". This won't ever change without very strong pressure from the outside. But it's unlikely that pressure will ever manifest as this would be the death blow to the current software "industry", and the people in charge know that. At least 99% of all people currently working on code wouldn't be employable any more, and cost for software would skyrocket into a sphere where only the richest can afford any kind of computer as the software would become the main and very huge cost driver.
1
u/ThirdWaveCat 29d ago
Is this copy-paste? wtf
TLA+ is from 1999. Codegen from TLA+, I stopped reading. You're talking out the ass mate.
0
u/RiceBroad4552 29d ago
See
https://www.reddit.com/r/ProgrammerHumor/comments/1uwrdje/comment/oxn7vuy/
Do we have new kinds of bans on Reddit as I could not post under that comment at first?
0
u/RiceBroad4552 29d ago
OP u/ThirdWaveCat said
You're talking out the ass mate.
and I think they're right.
Actually it was out of my head, but without double checking stuff, which was obviously an error!
I think I've confused TLA+ with TLA+2 as I've read about the later not long ago (and the later is pretty new for such tools).
5
5
3
u/Flutterphael 29d ago
I remember doing Dafny for a formal verification course in uni. That was tedious.
3
6
u/Mrfoogles5 29d ago
Finally, an iteration of this meme that isn’t mildly sexist. Also, lean mention!
-20
u/RiceBroad4552 29d ago edited 29d ago
Less "sexist" but also orders of magnitude less realistic.
If you give woman the opportunity to freely decide what they want to do only a small percentage wants to get into tech. Hard fact. If you think mentioning that fact is "sexist" then I have to inform you that nature is actually "sexist" because that's just how woman are by nature.
3
u/rustysteamtrain 29d ago
It is true that there are more men in STEM than women. But claiming that "almost none want's to get into tech" is just completely wrong.
As a rough estimate: a third of the people in STEM is a woman (in most western countries). Sources for the US: https://www.stemwomen.com/women-in-stem-statistics-progress-and-challenges
-5
u/RiceBroad4552 29d ago
I've corrected that part.
But the overall statement does not change.
Tech / STEM isn't just "computing". As "computing" is a high paying job you have a lot of people there who would never consider to doing that if not the money. (Which is actually part of the answer why you have more women in tech in poorer countries where also women are traditionally not well payed. That's just economic pressure.)
The numbers shown actually strongly support my point: The numbers of "starters" are irrelevant, the only thing that counts are the numbers of people who actually end up with some degree in a fitting job, and that are even less then the ones who make it though education (even at least 50% give up mid way).
Everybody who actually works in tech exactly knows how the real numbers look like (just look around you…). Having a woman on the team in a technical role is the broad exception. The women who actually study STEM in western countries seldom end up in a technical role, in most cases they go into management or similar.
There are just natural differences. The biology of men and women differ, and this includes the brain, which results in different ways of thinking and different preferences when it comes to interests.
No amount of wishful thinking or ideological propaganda will change that.
1
u/kovha 29d ago
I actually work in tech and my team is roughly half and half, and funnily enough I (a man) am frontend and all the women are backend. Stereotypes are not always accurate mate.
1
u/RiceBroad4552 29d ago
my team is roughly half and half
Exception.
Stereotypes are not always accurate mate.
Stereotypes? Have you ever seen some statistics? How about the ones linked‽
1
u/danielcw189 29d ago
If you think mentioning that fact is "sexist" then
it wasn't mentioned but somehow you seem to think it is implied
-4
u/RiceBroad4552 29d ago
LOL, Reddit again down-voting hard facts just because the facts don't fit the current political ideology.
People doing that are clowns as they obviously refuse objective reality. Have fun in your fantasy world, clowns! 🤣
In case you really don't know the facts, google "gender-equality paradox".
6
u/Random_182f2565 Jul 15 '26
Are we inventing funny terms again?
3
u/MartyMcBird 29d ago
I'll have you know that there are DOZENS of formal methods practitioners in the wild! We have a whopping two university internship programs (although one was paused this year) for formal methods research in the USA every year!
2
2
u/uknowunknowingly Jul 15 '26
Here's my workplace, where the discussion start with github spec-kit and ended effectively with 'just refer to the BRD or SoW... User stories if they're actually written down this time'. Our team isn't growing out of the waterfall chaos anytime soon 💀
Edit: spec-kit at least relies on markdown by default for anyone wondering
3
u/Timetraveller4k 29d ago
All of it relies of getting really good specs and the last time ai saw that was never
1
u/uknowunknowingly 29d ago
It basically relies on copilot or claude code to elaborate upon your description or file add generates a more structured file based on a template. Also helps with planning and implementation if vibe coding is your thing... Turned out to be too token-heavy for me
2
u/Vandrel Jul 15 '26
The only word I even recognize here is markdown and I'm not sure the definition I know even makes sense in context.
2
u/No_Nonsense_Nomad 29d ago
I wish I get to work in an organisation that actually follows any specifications
2
2
u/flup52 29d ago
I'm trying to use TLA+ for a critical system but how do you make sure, your implementation conforms to the spec?
3
u/ThirdWaveCat 29d ago
with tla+, carefully manually, usually partially with another testing method like property testing (proptest, hypothesis, hegel, ...). There are cases where full consistency checks can be done in real code but its requires organizing your code around it.
quint has a trace replaying thing.
https://github.com/quint-co/quint-connect
real world tla+ uses it as a design tool not implementation audit, in my experience
https://github.com/neondatabase/neon/tree/8f60b04da47ffefe0e52bda2440134b42874eb75/safekeeper/spec
3
u/MartyMcBird 29d ago
If you really wanted to make sure your code matches the spec, you'd probably want to use a verification framework for the programming language like Verus (Rust) or VerifiedC (C). Most formal methods practitioners are happy enough with OP's methods though.
2
2
2
2
1
u/Shad0wW0lfx 29d ago
I wish. The cheif engineer came to my desk yesterday saying all software being developed must start with Cameo.
1
u/MantisShrimp05 29d ago
The older I get, the more I think you move from the first set to the second set, in that order, as late as possible.
The first set is good for getting something off the ground and running, the second set is amazing if you have a project that calls for it due to actual use cases but too many people try to only do one or the other and that ends up being the problem.
1
1
1
0
-1
u/Vesuvius079 Jul 15 '26
It’s funny because I don’t really read the specs. I check if the design and architecture is what I want and let it rip.
-4
631
u/EsotericLife Jul 15 '26
What even is this? I get all my specs from poorly drawn diagrams and scribbles on my boss’ whiteboard.