Hacker News new | past | comments | ask | show | jobs | submit
computably | on: LLMs are making formal software verification feasible at a much larger scale
What you're describing is a language that can effectively take a high-level design doc (limited to a formal language representing a pseudo-English-subset) and compile to almost arbitrarily complex, formally verifiable systems. I say systems because you're also implying these could essentially orchestrate distributed systems.

Which, if that were really possible, would be pretty good evidence of AGI. Or, at least, the end of 6-7 figure software engineer salaries. Conversely, I think it's a pipe dream. Writing a compiler that actually works well across such a broad range of hugely complex behaviors would itself be absurdly complex.

yazaddaruvala | parent | next
AGI will accelerate it, but way before agentic development I learned this was the future when I worked at Amazon. I no longer have access to the internal talks about it (amazing to watch) but here is a public link worth reading:

https://aws.amazon.com/blogs/storage/how-automated-reasoning...

tkz1312 | parent | next
You don't really need compilers anymore. LLM's can write programs over any AST and provide an equivalence proof provided you have good semantics for the source and target.
loading story #50207783
loading story #50204479
loading story #50204901
est31 | parent | next
Also you would probably want to cache the compiler's output in git because running that compiler would take a long time, and you probably want the compiler's output to still be inspectable to human inspection. In the end that compiled artifact would look a lot like source code.

I think Rust's success in the AI space shows how useful formal proofs are, as Rust provides something very similar to that. Both because it helps with the understanding of LLMs, as well as with trusting the LLMs are not violating any basic properties (like please no nasal demons if the user sends a buffer larger than the allowed amount).

loading story #50204826
loading story #50206080
anthk | root | parent
We've got inform7 with an English like language generating complex inform6 OOP optimized code since a few decades and the i7 compiler might even run under a Pentium II with 128MB of RAM under NetBSD. I6, under 32 and a Pentium. And maybe even less. ZMachine games themselves (the biggest v8 ones) under the Frotz interpreter, under a 486 and 8MB (with FreeDOS and Frotz). Or maybe an Amiga or a m68k Mac with the same amount of RAM.

Now imagine what AMD64 machine can do with 2GB of RAM (minimum baseline for legacy, maybe some C2D computer) today.

loading story #50204533
anthk | parent | next
Check Inform7 for text adevntures. No AGI nor AI needed. On Inform6, it's a dumb simple OOP language where the structure it's almost self-evident. Classes, in-game objects with real-life attributes (enterable, a container for other objects, non-movable/pickable scenery and so on).

PD: inform7 can run on an RaspPi B+ or 25 year old PC's like nothing, and i6 down to 30 year old ones. The ZMachine adventures themselves, from any 16 bit computer and up.