HNHacker News
TopNewBestAskShowJobs

lastmjs

73 karma · joined May 12, 2016

submissionscomments
lastmjs··on Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
I don't know yet, but with Lasm I'll be spending a lot of effort finding out. And hopefully I'll get some help.

For me Lean is the key that has unlocked the idea of formal verification for general-purpose software engineering...before it was just an amazing technology that I couldn't practically touch in my profession and personal projects. That's changed now.

lastmjs··on Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
Yes, one way to think of it that I think is very useful is that all software engineers who have embraced AI agents as the core tool through which they design, build, and solve practical real-world problems are agentic engineers...with an emphasis in software engineering.

The background in software engineering is incredibly useful, currently, especially as a means to judge the evidence that the agents present attesting to the correctness of the solution.

Do I feel bad about misusing the engineering term? Maybe...but am I misusing it? How do you define engineering? If using science, math, logic, and technology to solve practical real-world problems is engineering...then?

lastmjs··on Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
It's even supposed to mean this: https://news.ycombinator.com/item?id=50302599
lastmjs··on Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
I believe that software engineering will be considered solved for the vast majority of current software development sometime in 2027.

I'm setting myself up to take advantage of the most useful tool ever created, the AI agent, to create in whatever way I want and is necessary in the future. Software engineering may not be necessary in the future, at least not for a lot of normal software application development we see today.

lastmjs··on Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
Hi. Well, sure I could consider myself a software engineer with an emphasis in agentic engineering...but that's not how I see the world now.

Check out this episode from my podcast to understand my thinking more: https://millillion.org/podcast/001-we-are-all-agentic-engine...

The extent to which AI is performing essentially all of my code generation and a large portion of the actual software engineering is astounding. My role has largely evolved into perfecting the process by which the agents are guided into well-architected solutions, manually testing their outputs, judging the artifacts that they present as evidence of clean code and robust implementation, and understanding business workflows well enough to guide the agents to a good working app that can be used by people.

AI is so integral to everything that I do professionally and in the software engineering space, it's outrageous. And I can apply those skills with extreme effectiveness to other areas outside of software engineering, such as tax preparation, legal document design, and my associates to CAD, energy flow analysis, structural engineering, etc.

I believe it is a very useful way to set ourselves up for our current reality and the future of work that is increasingly upon us.

I typed "define engineer" into Google just now and it's AI result says: "An engineer is a professional who applies science, math, and technology to design, build, and solve practical real-world problems"

Is that not very close to what I and many others are doing with AI now? The agents are the technology that I'm using to design, build, and solve practical real-world problems.

We need to adopt the agent as the core engineering tool now to be most effective moving forward, so I believe that we should all consider ourselves agentic engineers or developers with an emphasis in our previously acquired skillsets.

lastmjs··on Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
That's what hooked me on Lean. Lean is a general-purpose software development language, not just a formal verification language. This is powerful.
lastmjs··on Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge
Thank you! Many more example apps with many more proofs are coming.

Also everything you've seen so far in Lasm at the Lean source code level has had almost no human honing from me. I'm a beginner to Lean, but I'll be honing the Conduit app and also bringing more example apps in.

The extent to which we can formally verify traditional web frontend and backend code is something I'm very excited to find out. My personal first goal is to be able to delete much of my test suites and replace them with Lean theorems.

lastmjs··on Lasm: Write formally verified web apps in Lean, deploy to Node, serverless, edge
Lasm has been my dream for a good part of 2026.

I firmly believe that formal verification is the next evolution of software engineering and programming languages. This next wave will largely be enabled by the incredibly intelligent LLMs that understand formal verification and its programming languages.

Lean is one of the most popular languages that allow for formal verification, and to me is incredibly powerful because it is a general purpose programming language with formal verification built directly into it.

You can build general purpose software in Lean, and formally verify it in Lean. Amazing.

Lasm brings Lean to the browser, Node, serverless, and edge environments (and more). The idea is that you can now write web apps, frontend to backend, in Lean and formally verify these apps.

Imagine an Express server or Hono server, running on Cloudflare Workers, with formal verification of its specification.

I'm an agentic engineer with an emphasis in software engineering, and Lasm was built mostly by Claude Opus 5.5 with my high-level direction.

lastmjs··on RustPython
We've been using RustPython as the Python interpreter for our project Kybra, which is a Python environment for the Internet Computer Protocol (decentralized cloud, where all programs are automatically replicated across 13-40 nodes). Wasm is the runtime environment on ICP.

It's been working quite well, though lack of C extensions is a problem. We're hoping to move to CPython once the wasi and C extension support is there.

But the project works, compiles to wasm32-wasi, and can execute on the live ICP network: https://github.com/demergent-labs/kybra

lastmjs··on Zwitterion: a web dev server that lets you import anything
I believe most if not all of the missing features can be addressed and eventually Zwitterion could replace Webpack. I believe that non-bundlers will replace bundlers. Also, not all of the features Webpack provides I believe are necessary (like bundling) in forward-facing applications.
lastmjs··on Zwitterion: a web dev server that lets you import anything
Great feedback on the README, thank you
lastmjs··on Zwitterion: a web dev server that lets you import anything
Alright, I'm feeling bad about have a misleading title and I'd like to fix it. I can't change the title now without removing this post and reposting it. Do you have a suggestion for what I should do?
lastmjs··on Zwitterion: a web dev server that lets you import anything
Exactly
lastmjs··on Zwitterion: a web dev server that lets you import anything
If you really want it you can open and issue and try to be convincing...but I'm pretty set on moving forward with just ES modules. I attempted this in the past and compiling CommonJS to ES modules was pretty complicated at the time. I'm not sure it would be worth doing, but perhaps it would be. I want Zwitterion to be forward-facing
lastmjs··on Zwitterion: a web dev server that lets you import anything
Zwitterion could add support for .svelte files rather easily
lastmjs··on Zwitterion: a web dev server that lets you import anything
I encourage you to try Zwitterion, that's exactly its goal
lastmjs··on Zwitterion: a web dev server that lets you import anything
No you're good! I just want to come through this with my integrity intact. Also, the browser-compatible Node.js libraries you spoke of above, those can be added to Zwitterion as well. I had something similar done in a previous version, but I removed it. All of these comments are going to be Zwitterion's roadmap, so thanks again.
lastmjs··on Zwitterion: a web dev server that lets you import anything
Thanks for the feedback, seems like sourcemaps will be needed, shouldn't be a problem: https://github.com/lastmjs/zwitterion/issues/266

Zwitterion is not a bundler. I believe the world will move away from bundling, and that Zwitterion can replace Webpack eventually.

lastmjs··on Zwitterion: a web dev server that lets you import anything
True, but you lose the enormous benefits of things like TypeScript and the latest JS features. We need the good old days of our dev process combined with the good new days of language features
lastmjs··on Zwitterion: a web dev server that lets you import anything
I don't plan on supporting common.js. See this issue for CSS and images: https://github.com/lastmjs/zwitterion/issues/265

I will most likely add those soon. I will also be exposing a plugin system (currently it's just internal) that allows for others to add functionality that Zwitterion core will not support.

lastmjs··on Zwitterion: a web dev server that lets you import anything
I think it's simpler. No bundling. You don't have to include a bundle file, you just include files directly as you would have without a bundler. That may seem like a trivial difference, and it could be, but it leads to simpler code and less of a delta between what you think is happening with your modules and what actually happens at runtime.
lastmjs··on Zwitterion: a web dev server that lets you import anything
Exactly. Zwitterion relies on ES modules in production and development, so bundling is not strictly necessary. See the README for information on performance implications.
lastmjs··on Zwitterion: a web dev server that lets you import anything
Yeah I've been seeing that too. I've definitely been working on it recently, I just stopped using semantic release which was doing GitHub releases, and I've switched to just using tags...which apparently aren't releases. I'll need to sort that out. Definitely under active development!
lastmjs··on Zwitterion: a web dev server that lets you import anything
Exactly. You don't need any of that if you don't want it. You can write everything in your HTML file if you want, put your script in a script element (though there will be no compilation of the script element, if you want that it needs to be in its own file).
lastmjs··on Zwitterion: a web dev server that lets you import anything
You should be able to set the MIME type: https://github.com/lastmjs/zwitterion#headers-file

In the case above, you would need to say type="module", because you are importing a module even if it is tsx. But, you should be able to set the MIME type for .tsx files with a custom header file

lastmjs··on Zwitterion: a web dev server that lets you import anything
Hmm...excellent feedback! Thank you. I hope I wasn't dishonest with the title. I do believe Zwitterion has the potential to rival and replace Webpack eventually.
lastmjs··on Voluntary universal subscriptions for podcasts
You have an interesting take that I'll definitely consider, thanks for being so thorough. Also, if you want to see this project come to life, would you mind jumping into the Telegram group? https://t.me/podcrypt

I won't start working on it until we have 100 people there

lastmjs··on Voluntary universal subscriptions for podcasts
Thanks for the feedback. You will definitely be able to do something like you're suggesting. That's what I meant by "You'll be able to set how much you value each unit of time per podcast."
lastmjs··on Prisma – An open-source GraphQL API layer for your database
I think the point of this release is to open up operations outside of CRUD. I'm not sure if you've been following graph.cool, but they've been having a lot of churn over the past few months. The issue you bring up about CRUD has been addressed and is one of the main reasons for this new release, as far as I understand.
lastmjs··on Ask HN: What are the cons of Google Polymer?
You can use Redux with Polymer projects. I've created an element for that: https://github.com/lastmjs/polymer-redux-store