I’m a bit puzzled by this kind of comment, which pops up every time someone mentions getting some work done while out in nature.
What it seems to miss is that we get to walk around while doing some work, not the other way around. The alternative would be being stuck at a desk or in a meeting room, not quietly enjoying nature on a day off.
What is the reason you couldnt use your laptop on the beach to do work in 2019? Probably mainly that you are either working or enjoying nature, not both, and if you're working, then an office with reliable Internet, no wind or sun in your face, etc, is more suitable/efficient.
Put another way: if my twin and I are both working at competing firms doing the same job, but I do it via satellite phone while hiking the PCT and he does it from in front of a keyboard, there is no way he's not getting more done, even with AI. The bandwidth of voice/text to speech is a tiny fraction of visual.
Thanks for asking! I have had pain in my back and and shoulders and hands from being deskbound since I was 18 and it is a constant balancing act to get in enough exercise to offset the work in front of the computer. I have also used standing desks, 500$ ergonomic keyboards, and forced remote work during covid was a godsend because I could take regular breaks to pace my living room while I was worried to be perceived as unfocused if I did this in the open space. Speaking of living room, working on my TV from a distance of 2m alleviated eye strain too, compared to using the laptop screen or even a secondary monitor at my desk.
Believe it or not, it was not practical to take my gear into nature haha. But with the advent of agentic coding (and stt solutions like handy), I can be productive with much less typing and equipment.
I have considered leaving the tech sector because of the aforementioned friction, and just like in my message above, I don't think we are considering the same dilemmas. OP said work vs contemplation, I said indoor work vs outdoor work. You mention productivity trade-offs, but for me working in tech used to feel physically unsustainable.
The counterfactual is impossible to prove here, but I think it’s at least plausible that this poster, who I guess lives near the beach, could have enjoyed their morning coffee on the beach
Strongly agree. I see the need to understand as back pressure on the system that produces code and features: it limits output to what fits into a working mental model. Agents could turn tickets into code much faster, but I am building a product, and it needs someone who holds that model to steer it long term.
And when the job is done, I run retrospectives on old coding-agent sessions to find areas of friction and confusion. I also journal with pen and paper, as it's supposed to bring cognitive benefits, to help me stay on top of things.
Looks like v3.0 just dropped, though after a very cursory glance at the release notes, I wonder what motivated the major bump specifically.
I deploy on a single machine with Docker, as my apps are both small scale and non-critical (people pay for them though). Kubero popped up when I researched how I would do a multi-server setup should the need for High Availability arise. It might flatten the learning curve and drop the operational overhead of Kubernetes enough to push me in this direction.
As for running the cluster myself, I probably would try to run K8s on talos.dev as well.
I will peruse your learning path when I am done with writing my master's thesis. Thanks for putting it together!
Lots of bullet points and keywords about the "What" : provable recursion, next-token prediction, and formal verification... and all items in "What makes it special". Can you provide a practical motivation, even speculative for people like me who have little time? Not necessarily "What use does it have right now", but "The qualitative difference with other models might enable use case XYZ in the future".
I have noticed it is low power and this is great in itself. What does the more rigorous formalism bring to the table? No snark at all, I am fascinated by formal methods, but still looking at them from afar.
Thanks for the thoughtful question— and good luck wrapping up the thesis!
Here’s the shortest road-map I can give for why the heavier formalism matters once you already have low-power execution nailed down.
First, the grammar + proof layer lets you guarantee properties that today’s neural LLMs can only hope to satisfy. Because every production rule carries a machine-checkable proof obligation, you can show that responses will always terminate, stay within a memory budget, or never emit strings outside a whitelisted alphabet. In practice that means the model can be certified for safety-critical or compliance-heavy settings where a probabilistic network is a non-starter.
Second, the same proofs make the system auditable and patchable by domain experts instead of ML engineers. An agronomist can inspect the maize-disease module, see that the recursion proving “all advice paths end with a referenced citation,” and swap in an updated pest table without breaking that guarantee. The edit-compile-prove cycle is minutes, not GPU-months.
Third, formal hooks open the door to hybrid workflows. You can embed the micro-LM inside a larger pipeline—say, a standard transformer model proposes a draft, and our verified core acts as a “lint pass” that repairs grammar, checks facts against a local SQLite cache, and signs the result with a proof artifact. That could be huge for regulated industries that want the creativity of big models and the certainty of formal methods.
Finally, on the speculative side, once responses are proof-carrying you can imagine device-to-device marketplaces of small, composable skills: my weather module proves bounds on forecast error, your SMS gateway proves it redacts PII, we link them and the combined proof still holds. That’s hard to do with opaque neural weights.
So the low-power story gets us in the door; the rigorous formalism is what keeps the door open when reliability, certification, or composability become the bottleneck. Hope that gives you a clearer picture—and when the thesis dust settles I’d love to hear your perspective on how formal methods could push this even further.
My work is about inferring solutions to Constraint Satisfaction Problem by using belief propagation in the corresponding constraint network, a few keywords caught my eye here :)
Do you have any illustrative example so I can understand better what you are hinting at?
Not exactly the approach your describing, but Futhark[0] offers an alternative to CPU execution, it compiles to CUDA or OpenCL to run on GPU (or multi-threaded CPU).
That one I am aware of, as language geek, I am always curious to GPU alternatives that aren't always the same old story only C and C++ get to party, which is actually an advantage of CUDA's polyglot approach.
What it seems to miss is that we get to walk around while doing some work, not the other way around. The alternative would be being stuck at a desk or in a meeting room, not quietly enjoying nature on a day off.
reply