lastmjs
Joined 10 years ago
Karma
72
Submissions
53
Member since
May 12
Recent submissions
Comment · 1 day ago
Comment · 1 day ago
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?
Comment · 1 day ago
It's even supposed to mean this: https://news.ycombinator.com/item?id=50302599
Comment · 1 day ago
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.
Comment · 1 day ago
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.
Comment · 1 day ago
That's what hooked me on Lean. Lean is a general-purpose software development language, not just a formal verification language. This is powerful.
Comment · 1 day ago
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.
Comment · 1 day ago
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.
Comment · 2 years ago
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
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.