Hacker News Reader

uptodatenewson Anatomy of a Lean proof for software engineers

Here's also a book list

https://rcsnyder.github.io/open-frontier-curriculum/07-resou...

uptodatenewson The internet discovers TLA+. Now what?

Plugging this again if you want a quick visualizer client side program to go back and forth with an ai. Granted opus 5.5 can probably 1 shot this now

https://tlaplus-process-studio.com/

https://github.com/RCSnyder/tlaplus-process-studio

Also the hard part is connecting the tla+ spec to the implementation code with traces

uptodatenewson GPT-6 Astra

You want a computer program to be able to take a single phrase and execute decade long journies?

Who will be responsible for the outputs and side effects of such a closed loop system?

Half of those the agent fleet systems can do right now.

These are things it cant do and will not be able to do without human labor and long running human vision:

https://rcsnyder.github.io/open-frontier-curriculum/05-front...

uptodatenewson No country for mediocre mathematicians

Yeah this just means 1000x more people can become phds if theyre willing

uptodatenewson No country for mediocre mathematicians

Im going with this... scifi stuff still requires engineers. Its laughable and insulting to think these billionaire owners are going to make robots and llm loops to get real shit done

https://rcsnyder.github.io/open-frontier-curriculum/

Ya "claude can you build me the next cern Thanks"

uptodatenewson Cloudflare OS: an open platform for agents, apps, and work

I tried to make something in the same spirit

https://github.com/RCSnyder/open-pincery

uptodatenewson Hunting a 16-year-old SQLite WAL bug with TLA+

You run into Rices theorem if you try to apply it too heavily.

I made https://github.com/RCSnyder/tlaplus-process-studio

https://tlaplus-process-studio.com/

For local only high level modelling. Its not a full tie into the actual model checker, but its meant to serve as a first step into system modelling for state machine modelling for beginners

uptodatenewson Can LLMs model real-world systems in TLA+?

Whoa didn't even know cool

uptodatenewson Show HN: Marky – A lightweight Markdown viewer for agentic coding

I said just keep it in the repo like scaffolding.

Is software ever done?

Why remove the dev notes for the future agents?

https://github.com/RCSnyder/lights-out-swe

uptodatenewson A sufficiently comprehensive spec is not (necessarily) code

This is exactly why I built these two things

https://github.com/RCSnyder/tlaplus-process-studio

This is to extract the bare minimum state machine out of users is tla+

https://github.com/RCSnyder/lights-out-swe

And pop that into input/docs/* with any other user requirements

And add your tech stack in preferences.md

And say "build me the thing described in input"

And it goes for it