Comment by tombert
2 months ago
I'm mostly diving head first into formal methods again. Mostly TLA+, but a bit more Isabelle as well.
I haven't really forgiven myself for dropping my PhD; I think it was the right decision at the time, but I also kind of wish I had pushed through it. I'm going to see if I can at least get a few papers published.
I've also had some fun getting Claude to create LSP servers for different languages, which it has been pretty good at, and that's nice; having good integration with Vim makes a language a lot more fun for me.
Oh, I also presented at LinuxFest two weeks ago: https://youtu.be/HmcVJWyOwJQ?t=6623
Are you familiar with FizzBee. I think formal methods is already very hot right not with more demand for proving AI generated code isn't garbage.
(Even if you're hand writing people are going to assume or suspect it's LLM gen.)
I am!
The author of FizzBee reached out to me about a year ago on LinkedIn actually, because I gave a talk on TLA+ a few years ago.
I haven't really played with it yet (outside of the few examples on their site) because I'm already pretty entrenched in the TLA+/PlusCal world, but it is very likely that FizzBee might be a better fit for software engineering circles; the incremental testing is pretty neat, to a point where I kind of want to steal the that and port it over to TLA+/TLC. Probabilistic testing seems pretty cool too.
If I were getting into Formal Methods today for the first time, I would almost certainly be using FizzBee and/or Alloy.
I have knowledge of FM primarily from HackerNews posts about it.
As someone lacking your academic background in it could you give me some advice on a good starting point, or perhaps papers/materials that are absolutely unskippable/foundational to understanding it, maybe a good learning exercise for utilizing FM?
3 replies →