hwayne

42 ms·

451.
by hwayne 7y ago
I like these a lot! I'm seeing them less as "interview questions", which they'd be terrible as, but as "annoy your friends questions" after you've all had a couple drinks. One I heard a while back: "Y
452.
by hwayne 7y ago
Wikipedia has a great article on this: https://en.wikipedia.org/wiki/Writing_in_space
453.
by hwayne 7y ago
To clarify, it was an email newsletter. The YOW! thing had just gotten published so I got that out of the way before diving into the meat of the newsletter post, which was about LP.
454.
by hwayne 7y ago
I'm excited to see this!
455.
by hwayne 7y ago
I wrote a few case studies here: https://www.hillelwayne.com/post/business-case-formal-method... . They're case studies that are targeted towards bosses, so focus on how it saves time and money. A couple more I kno
456.
by hwayne 7y ago
Mostly it's a lack of education and UI work. The Alloy IDE, for example, doesn't have line numbers. There's also no CLI for Alloy. That said, it's an excellent tool and I've found it very useful when doing formal mo
457.
by hwayne 7y ago
One of my favorite war stories was losing a client after we spent two days trying to model their problem and discovered they didn't actually know what they wanted and they decided to just scrap the project and do something else
458.
by hwayne 7y ago
Code review. Lots and lots of code review!
459.
by hwayne 7y ago
Every time this frontpages I feel super shitty about not getting back to it. I've learned a _lot_ about how to teach TLA+ in the past three years, and there's a lot I know I can improve about this guide. One of these days, I promi
460.
by hwayne 7y ago
As part of a project I interviewed a lot of "crossovers": people who worked as both traditional engineers and software engineers. According to everyone I talked to, requirements volatility happens everywhere. Two civil engineers h
461.
by hwayne 7y ago
Have you talked to civil engineers? I have. This happens all the time.
462.
by hwayne 7y ago
And software engineers don't have to deal with half their tensile bolts having 90% of the tensile strength built they don't know which half, or the bridge collapsing because they mixed brass and zinc bolts[1], or hurricanes... Tur
463.
by hwayne 7y ago
I've met at least two engineers who had to move bridges after they were built.
464.
by hwayne 7y ago
The seL4 code didn't start out as C. First they wrote the whole thing in HOL (an ML dialect), then translated that to Haskell, then translated _that_ to C. Verifying code is correct is Just Plain Hard.
465.
by hwayne 7y ago
Agreed- that's why I said in the beginning I'm only talking about design verification. Verifying code is a long way off from going mainstream. I talk about the limitations of code verification in this essay: https://www
466.
by hwayne 7y ago
It's possible to use TLA+ for complex serial systems, and it can def help there. The thing is that TLA+ is designed to be good at modeling concurrent problems, problems that have a lot of specific challenges you don't see in seria
467.
by hwayne 7y ago
> Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night! I'd _hope_ you'd have those processes, working on space flight and all :P. Good processes > good
468.
by hwayne 7y ago
> If you're not verifying the actual code, then how do you prevent bugs creeping during whatever happens between verification and actually writing the application code? Code review! So, SO much code review. Also testing and type sy
469.
by hwayne 7y ago
seL4 comes to mind. Also IronFleet[1], which is small but end-to-end verified in Dafny. People tend to verify the cores of complex systems, not the entire thing. See here[2] for more on that. I suspect there'd be a lot of stuff using e
470.
by hwayne 7y ago
The design of S3 was formally specified, but not the actual code.
471.
by hwayne 7y ago
They don't actually give any reasons why LaTeX is wrong. They just say it is. I mean LaTeX has issues, but you gotta dive into them, man. I've written a book in a mix of Microsoft Word and Markdown, and they both had the same prob
472.
by hwayne 7y ago
> So what? TLA+ still achieved something that no other formal logic had before it (AFAIK). What I'm saying is that either TLA+ wasn't the first (Z was earlier), _or_ TLA+'s success has much less to do with anything especia
473.
by hwayne 7y ago
> BTW, you mentioned TLA+. TLA+ also requires some effort, although significantly less than Lean (or Isabelle, or Coq), but TLA+ has made a historical breakthrough in formal logic. From its inception in the late 19th century, and even fr
474.
by hwayne 7y ago
We were giving imperative programs formal semantics well before we started using monads. See Pneulli's "The Temporal Logic of Programs" ( http://dimap.ufrn.br/~richard/pubs/dim0436/papers/pn
475.
by hwayne 7y ago
Check out Marianne Bellotti's work. She recently gave a talk at Strange Loop on writing specifications of existing systems: https://www.youtube.com/watch?v=oMSmkRGzQ64
476.
by hwayne 7y ago
> (one dev's main complaint was that he was forced to use Eclipse, I don't know if integration has now happened with other IDEs since then) There are a few projects to make this more accessible. We have vscode: https:/&#
477.
by hwayne 7y ago
I've read parts of Holzmann's Spin book but haven't actually tried to apply any of it. Without some experience I can't really compare other tools to it. Also I've forgotten like half the language already :/ The
478.
by hwayne 7y ago
I've seen plenty of people use TLA+ to understand systems better without writing refinements. I also think you're in a good position to show comparative models between TLA+ and Spin or NuSMV, to show that the other two are more th
479.
by hwayne 7y ago
If you know good introductions to those tools, I'd be happy to look! Most of my experience is in things like PRISM, Alloy, TLA+, etc, and I don't have experience with those three. At least on a quick search, one difference between
480.
by hwayne 7y ago
I'm now _really_ curious as to how many people who use and value TLA+ have actually used refinement. I've used it, you've used it, Lamport and (probs) Merz and Markus have used it, most other people I've talked to haven&

More ›