News for hackers. Stuff that matters.

lastmjs

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.

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?

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.

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.

That's what hooked me on Lean. Lean is a general-purpose software development language, not just a formal verification language. This is powerful.
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.

Show HN: Lasm – Write formally verified webapps in Lean for Node/serverless/edge

https://github.com/Millillion/lasm

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...

( Read More... | 21 comments | 15 points | on HN )
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.

Re:RustPython on Wednesday February 07, 2024 @11:24AM (#39290469)
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

Query Ethereum: chain analysis from a browser tab

Hey everyone, I've been working on a new prototype project, https://queryethereum.comIf you want to jump straight into trying some examples, use this GraphQL bin: https://www.graphqlbin.com/v2/1GmVUn You can run all of those queries directly from the browser.Essentially Query Ethereum is a GraphQL API to Ethereum's blockchain data. It makes it very simple to get aggregate information like block...

( Read More... | no comments | on HN )
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @12:22PM (#21914985)
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.
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @12:10PM (#21914869)
Great feedback on the README, thank you
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @12:09PM (#21914860)
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?
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @11:56AM (#21914733)
Exactly
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @11:56AM (#21914726)
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
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @11:50AM (#21914671)
Zwitterion could add support for .svelte files rather easily
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @11:48AM (#21914649)
I encourage you to try Zwitterion, that's exactly its goal
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @11:44AM (#21914607)
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.
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @11:42AM (#21914584)
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.

Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @11:41AM (#21914568)
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
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @11:40AM (#21914558)
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.

Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @11:38AM (#21914543)
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.
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @11:35AM (#21914509)
Exactly. Zwitterion relies on ES modules in production and development, so bundling is not strictly necessary. See the README for information on performance implications.
Re:Zwitterion: a web dev server that lets you import anything on Monday December 30, 2019 @11:34AM (#21914498)
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!

Older »