Posted by david927 1 day ago
Ask HN: What are you working on? (May 2026)
s/import SwiftUI/import OmniUI/
As long as you aren't using Apple platform specific libraries like Vision, you should be good for the most part. I am going to make my Gopher browser (https://web.navan.dev/iGopherBrowser/) the first target. I have done some extra stuff like reimplementing CoreData/SwiftData to make it work on Linux.
I am going with Adwaita instead of pure GTK because I like the opinionated approach they have with their design language. I think the reason SwiftUI works is because you can get pretty looking apps without thinking too much.
Projects like adwaita-swift, and swift-cross-ui do exist, but I want my library to be a drop-in replacement. I don't want to be inspired by SwiftUI, I want to use SwiftUI everywhere!
I plan on separating out the UI portions to its own repo and then polish it up
yayauptime.com (named after the first words of my friends kid) YAYA!!
if someone needs a free signup: https://www.yayauptime.com/auth/signup?invite=YAYA-BETA-2026
Tinder meets Discord and, somehow, they have their way with Uber/Calendly.
It's live if you want to test it: https://jynx.app/
Let me know what you think of it. The main goals I want to achieve are: 1. help with social isolation 2. help e-sport team with sourcing and organizing
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
(Even if you're hand writing people are going to assume or suspect it's LLM gen.)
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.
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?
------
If you're just getting started, I recommend checking out my former advisor's book: https://www.amazon.com/Software-Engineering-Mathematics-Sei/...
I found this book to be fairly easy to read through, and gives you a rundown of a lot of the notation and concepts that pretty much all formal methods systems require.
------
TLA+ is a decent enough language. I recommend going through Lamport's video series on it to start: https://lamport.azurewebsites.net/tla/learning.html
I don't know what aspect of Formal Methods that you want to focus on; most of what I've done is with distributed systems stuff, but TLA+ can and has been used for low level things like circuit modeling. I can't tell you where to learn about that.
I think Hillel Wayne's learntla website is pretty good to get a few more practical examples: https://learntla.com/. I actually thought his Practical TLA+ book was a bit better for that though: https://www.amazon.com/Practical-TLA-Planning-Driven-Develop...
Both of those resources are more PlusCal focused. PlusCal is a C/Pascal-like language that compiles to "raw" TLA+. A lot of people like it more, I go back and forth.
If you care more about the more theoretical aspects of TLA+, Ron Pressler's "TLA+ in Practice and Theory" blog series is great: https://pron.github.io/tlaplus
Additionally, I recommend looking for the papers by Stefan Merz. Here's a good one to start, but he has a bunch: https://members.loria.fr/Stephan.Merz/papers/tla+logic.pdf
------
If your goal is to model concurrent systems, getting an understanding of CSP is worth doing. I liked Roscoe's book on it: https://link.springer.com/book/10.1007/978-1-84882-258-0
If you go deep into that, I recommend looking at the extension "tock-CSP" that adds timing semantics.
-------
If you're interested in the most theoretical aspects of formal methods, the only one I've done with any kind of intimate detail is Isabelle.
Isabelle is much more of a "math proof" thing than a "computer science" proof thing, but there are plenty of computer science things for it too. If you want to get started with the Isabelle/HOL language, the Concrete Semantics book is the normal recommended starting point: http://concrete-semantics.org/
------
This is mostly my history, there are many other paths but I can't really speak to those with any confidence. Hope this helped!
ETA:
Just to add, while I did go to school later for formal methods, I actually started learning this stuff while I was still a dropout from my undergrad. I eventually got my bachelors and masters and then entered a PhD program, but for TLA+ in particular I was learning it without any completed education, so this stuff is definitely approachable even without a ton of letters after your name.
I shared earlier in the thread about the learning app I'm working on. I already have a learning path created in it for Formal Methods. I will be taking each of your points and tracking my progress to completing them.
Just wanted you to know your effort won't be unappreciated.
I have an email in my profile, feel free to contact me. Happy enough to answer questions to the best of my ability in the future.
a performance-first TypeScript checker written in Rust. Started 5 months ago and it's been mostly AI-written code. 99.8% tsc conformance test pass rate today. Single file benchmarks are 3–5x faster than tsgo.
oxc https://oxc.rs/ ezno https://github.com/kaleidawave/ezno
And when I say darkest recesses, I'm not referring to "0.1 + 0.2 != 0.3" (which is fairly well-known) but things like "so when you turn on denormal flushing, how exactly are you defining it because there's at least three different definitions..." Or also "does my emulator actually emulate floating-point behavior correctly, or is it delegating to the current hardware which might have a slightly different definition?"
Docker is...quite slow with large images. I've built a registry+pull client+buildkit builder to make it better. It splits apart layers, allowing for files to be shared between related images. In a robotics context, it can make pulls 10x faster. And in a cloud context, the format allows for pulling an image in 15 or 20 seconds instead of 60, without having to do a FUSE w/lazy pulling. Builds are faster, I store 7x less data due to better deduplication, I can run security scans faster due to not having to unpack tarball layers, etc, etc. I want to be the default registry for all ML related work, in the future.