3 ms·

I've been a big nerd for formal methods for quite awhile, and have been broadly unsuccessful in getting employers onboard. I have pretty cynical opinions as to

by tombert 2mo ago

I've been a big nerd for formal methods for quite awhile, and have been broadly unsuccessful in getting employers onboard. I have pretty cynical opinions as to the "why" of this, largely involving the fact that the vast majority of software engineers refuse to learn anything that they weren't explicitly taught in college, but regardless of the reason whenever I have tried proposing TLA+ in the past, people will nod along and wait for me to stop talking. I've had several managers say "they'll look into it", which was such an obvious lie that I don't know why they even bothered. I've "snuck in" TLA+ usage a few times. I gave up on getting anyone else to use TLA+, but as I've gotten more senior-level, I have been given a fair bit more leeway on how I approach projects and as such I have been able to budget myself a day or two to model some of the less-obvious bits of concurrency. All that said, I have had some luck with designing stuff with TLA+, then feeding the spec into Claude and getting that to implement the actual executable code. Maybe I'll be able to convince an employer that's a good use of time now.

plastic-enjoyer 2mo ago
> I have pretty cynical opinions as to the "why" of this, largely involving the fact that the vast majority of software engineers refuse to learn anything that they weren't explicitly taught in college, but regardless of the reason I think it's not only SWEs, but general persons that goe to college primarily to get a job, without having a natural curiosity for things.
- tombert 2mo ago
  Probably true, I've just only ever worked in the software engineering world so I cannot speak about anything else.
epolanski 2mo ago
Software engineers are rarely engineers at all, and pretty much never know anything about computer science.
- tombert 2mo ago
  Yeah, I've always been that "annoying math guy" for pretty much my entire career. This has always irritated me, because I'm not entirely sure what engineers feel that they bring to the table over a high school kid who bought one of those "learn C++" books. I always thought the value-add was supposed to be a better understanding of the theory and computer science and internals of how computers work, but that was evidently wrong. I've noticed that the "software engineers bragging about not knowing any math" trend appears to be dying, so that's cool, but now it has been replaced with the even more depressing "software engineers don't need to even need to know how to code anymore because you can just ask Claude Code to do it".
lioeters 2mo ago
> designing stuff with TLA+, then feeding the spec into Claude That seems to defeat the purpose of using TLA+ in the first place. It's taking a rigorously logical and proven specification, putting it through a black box (that you don't own and cannot inspect) with indeterminate and unknown process, to get executable code that may or may not have anything to do with the specs. Unless you feed the code back into something to verify that it corresponds with the specs? Is there nothing that can turn the specs into executable code directly and deterministically? Why involve a language model at all?
- tombert 2mo ago
  I'm not familiar with any general purpose TLA+->regular code exporter. I think there are a few proof of concepts but as far as I'm aware nothing that has been seriously suggested for production. I do audit the code it generates, but ultimately all I'm concerned about is the algorithm a lot of the time and since the transformation it's been generally ok. I feel like coding errors and implementation-of-the-spec errors are different things, and of course this would be an issue even if it were humans writing the code. If you use something like Isabelle then that has direct Scala and Haskell export. I like Isabelle but personally I find that for actual engineering problems it is often too cumbersome and TLA+ is much easier to get something done.
  - lioeters 2mo ago
    > would be an issue even if it were humans writing I see what you mean, that the conversion of TLA+ specs to code is error-prone in any case, regardless of who or what does the conversion. From what I've heard, an advantage of Lean over other major theorem provers is that it can generate actual executable code (apparently C), so you get the best of both worlds: formally proven specification and the implementation. In that context, I can imagine the use of language models to assist in the generation of specs, tests, and documentation - while a (formally specified) program deterministically compiles the specs to code, or maybe interprets the specs directly to run it as code.
    - tombert 2mo ago

by tombert 2mo ago

plastic-enjoyer 2mo ago

> I have pretty cynical opinions as to the "why" of this, largely involving the fact that the vast majority of software engineers refuse to learn anything that they weren't explicitly taught in college, but regardless of the reason I think it's not only SWEs, but general persons that goe to college primarily to get a job, without having a natural curiosity for things.

tombert 2mo ago
Probably true, I've just only ever worked in the software engineering world so I cannot speak about anything else.

epolanski 2mo ago

Software engineers are rarely engineers at all, and pretty much never know anything about computer science.

tombert 2mo ago
Yeah, I've always been that "annoying math guy" for pretty much my entire career. This has always irritated me, because I'm not entirely sure what engineers feel that they bring to the table over a high school kid who bought one of those "learn C++" books. I always thought the value-add was supposed to be a better understanding of the theory and computer science and internals of how computers work, but that was evidently wrong. I've noticed that the "software engineers bragging about not knowing any math" trend appears to be dying, so that's cool, but now it has been replaced with the even more depressing "software engineers don't need to even need to know how to code anymore because you can just ask Claude Code to do it".

lioeters 2mo ago

> designing stuff with TLA+, then feeding the spec into Claude That seems to defeat the purpose of using TLA+ in the first place. It's taking a rigorously logical and proven specification, putting it through a black box (that you don't own and cannot inspect) with indeterminate and unknown process, to get executable code that may or may not have anything to do with the specs. Unless you feed the code back into something to verify that it corresponds with the specs? Is there nothing that can turn the specs into executable code directly and deterministically? Why involve a language model at all?

tombert 2mo ago
I'm not familiar with any general purpose TLA+->regular code exporter. I think there are a few proof of concepts but as far as I'm aware nothing that has been seriously suggested for production. I do audit the code it generates, but ultimately all I'm concerned about is the algorithm a lot of the time and since the transformation it's been generally ok. I feel like coding errors and implementation-of-the-spec errors are different things, and of course this would be an issue even if it were humans writing the code. If you use something like Isabelle then that has direct Scala and Haskell export. I like Isabelle but personally I find that for actual engineering problems it is often too cumbersome and TLA+ is much easier to get something done.
- lioeters 2mo ago
  > would be an issue even if it were humans writing I see what you mean, that the conversion of TLA+ specs to code is error-prone in any case, regardless of who or what does the conversion. From what I've heard, an advantage of Lean over other major theorem provers is that it can generate actual executable code (apparently C), so you get the best of both worlds: formally proven specification and the implementation. In that context, I can imagine the use of language models to assist in the generation of specs, tests, and documentation - while a (formally specified) program deterministically compiles the specs to code, or maybe interprets the specs directly to run it as code.
  - tombert 2mo ago