4 ms·
I worked for a [Japanese] corporation, that took “formal methods” into overdrive. They made really, really good hardware, but it was extremely painful for us s
by ChrisMarshallNY 2y ago
I worked for a [Japanese] corporation, that took “formal methods” into overdrive.
They made really, really good hardware, but it was extremely painful for us software schlubs.
That said, I don’t know if it’s really possible to do really big stuff, with a team, unless you have some degree of formality.
Best practices are usually a good place to start, and I would suggest that the degree of necessary formality, is inversely proportional to the experience of the team. If you have a lot of really experienced engineers, in a mature team that has been together a long time, the formality is still there, but doesn’t need to be written down.
I usually work alone, or as the sole technical person, in a diverse team. I’m really experienced, and don’t write much down.
But I’m also really, really formal. It just doesn’t look like it.
- jxramos 2y agoDoes it come out instead in PR reviews?
- ChrisMarshallNY 2y agoIf I work alone, there aren’t any PRs. But I do spend a great deal of time reviewing my work; often going back, and tweaking and testing, for days. My testing code tends to dwarf my implementation code.
- spankalee 2y agoFormal methods is much more specific than formality and writing things down. There's a degree of proof that you achieve with formal methods that you don't even with design documents, reviews, and the usual tests.
- ChrisMarshallNY 2y agoAgreed, but also, “writing things down,” was a bit of a euphemism for the many, many aspects of a formal approach. The main issue is that we can get so wrapped up in the process, that we fail to get anything done. It’s a question of balance.
- nextos 2y agoThere are relatively lightweight methods which can be less taxing. For some domains, where requirements are frozen, iterative refinement of specifications to code can be easy and enjoyable. See for instance: https://raisetools.github.io/ https://raisetools.github.io/ My hope is that code assistants can make all this much easier by facilitating synthesis, you write the specification, and ML gets you the code. I have a fairly good toy prototype doing such a thing for the subset of a common functional programming language. Obviously, the difficulty is to scale it and make it practical.
- kccqzy 2y agoIt doesn't seem like you are describing formal methods. You seem to be describing plain old bureaucracy.
- ChrisMarshallNY 2y agoNot gonna argue. I know that, for many folks, these days, anything that imposes guardrails and boundaries, is considered “bureaucracy.” It’s funny, but there’s a heck of a lot of structure, in today’s software industry. It’s just not called “process,” or “formal methods.” It’s just “this is how everyone does it.” Pretty much a requirement, when your workforce leaves, every 18 months.
- yencabulator 2y agoI think you still haven't grasped what formal methods really means. Think proving your software correct with math, not "project management forces us to write documents". Formal methods is very much not "how everyone does it", currently.
- ChrisMarshallNY 2y agoWhy are you arguing? BTW: that corporation was very much into “proving right with math.” The Japanese really like math, and this corporation probably has hundreds of patents, describing testing and validation methodology. Watts Humphrey once wrote a book that described a personal formal methodology. Can’t remember the name, but it was a really big deal, in the 1980s. I think it went a bit overboard, but it worked well, for folks that followed it completely.
- yencabulator 2y agoYou keep saying things that don't sound like anything at all like what TLA+ is. Humphrey's Personal Software Process is just another project management methodology; nothing do with this topic.
- 2y ago