In my Django+Vue/TS/Inertia side project, I was surprised to see my agent know to build (use ts compiler in this context) after each change and it iterates till it gets it right. The Django code is not as typed, so I have to feed it a few error messages myself. Gotta unbreak my Mypy (python type checker) to keep my sanity.
In 2012, I felt the high of Scala programs working perfectly once it compiles. Now my TS code is almost there, and Django is somewhat behind.
Why Rust, which is just barely an improvement over a dynamically-typed language, when you can just as easily vibe to a language with a proper dependent type system?
Once you go down the spectrum then you have to start relying on tests, which end up indirectly validating the same things as the type system anyway, at which point you are no further ahead than having used a dynamically-typed language.
Partial statically-typed languages like Rust are pretty cool for things like highlighting basic mistakes in your editor as you type, automatic refactoring, etc. That is all very useful for humans writing code, even if a bit redundant on some technical level. But if an LLM is doing the work, none of that matters.
I asked several LLMs on your behalf and they all said "yes". But they might be a little biased.
Why not put them to the test? It is only a prompt away. Rust is an available extraction target for Rocq, so you can even integrate it into your existing codebase.
haha I shall. I like the idea of tighter constraints on LLM hence my enthusiasm for rust over python for vibecoding.
I did just try it and the first thing it did was try to download half a gig. Which is fine, except my fiber install is next week and I'm hotspotting off a phone. So that'll need to wait
...it did seem to fundamentally understand the ask though of "make me a plan to make a http hello world server".
Though at same time flagged that this isn't ideal
>Rocq/Coq is primarily for theorem proving; HTTP server implementation will be minimal
> Though at same time flagged that this isn't ideal
I suppose that depends how deep down the rabbit hole you want to go. HTTP is pretty minimal in and of itself. The complexity is due to it being layered on top of many other things, like TCP/IP, sockets, network devices, etc. Is it worth proving that your NIC functions according to spec? Probably not. But, if an HTTP server is what you are trying to build, like, parsing an HTTP request is quite suitable.
But a good case. I would suggest that Rocq is already proving itself. I expect by "make a http hello world server" you don't mean: First, invent the universe. Although maybe you do! Who knows? Your prompt is not clear. And since the type system is comprehensive enough to force you to actually think about what you really want, it is compelling you to be much more specific.
>I suppose that depends how deep down the rabbit hole you want to go.
I'm intellectually curious about whether a formal verification style vibecoding would work. It seems like the logical outcome of current trajectory - if compute increases exponentially then something where the LLM can just hammer away until it checks out seems ideal way of vibecoding while getting a bullet proof outcome.
Knowing absolutely nothing about formal verification I'm quite skeptical it's viable right now though. (For hobby projects, I'm sure the formal verification academics are having fun)
So still leaning towards rust as current optimal. I am ofc biased (python/rust is my preference depending on task).
>I expect by "make a http hello world server" you don't mean
There is no deeper thinking behind it. Selected it purely because if I ask a LLM to oneshot something without guidance I think keeping it simple and within training data is fair.
It's talking about Luau (gradually typed, https://luau.org/), not Lua.
Hopefully https://github.com/astral-sh/ty will make the Python typing situation better, but absent that, Python typing is... not great. Honestly even with that it feels subjectively very finicky.
icontract or pycontracts -like DbC Design-by-Contract type and constraint checking at runtime with or as fast as astral-sh/ty would make type annotations useful at runtime
> Mypyc ensures type safety both statically and at runtime. [...] `Any` types and erased types in general can compromise type safety, and this is by design. Inserting strict runtime type checks for all possible values would be too expensive and against the goal of high performance.
In my Django+Vue/TS/Inertia side project, I was surprised to see my agent know to build (use ts compiler in this context) after each change and it iterates till it gets it right. The Django code is not as typed, so I have to feed it a few error messages myself. Gotta unbreak my Mypy (python type checker) to keep my sanity.
In 2012, I felt the high of Scala programs working perfectly once it compiles. Now my TS code is almost there, and Django is somewhat behind.
Been vibecoding in rust for this reason. Even with the smaller amount of training data it does seem to produce less fragile code.
Why Rust, which is just barely an improvement over a dynamically-typed language, when you can just as easily vibe to a language with a proper dependent type system?
I think a big part of why rust vibe codes so well is the care the rust developers put into their error messages. It helps the ai a lot
Which languages would that be? Not being snarky, actually curious.
Rocq or another in that wheelhouse.
Once you go down the spectrum then you have to start relying on tests, which end up indirectly validating the same things as the type system anyway, at which point you are no further ahead than having used a dynamically-typed language.
Partial statically-typed languages like Rust are pretty cool for things like highlighting basic mistakes in your editor as you type, automatic refactoring, etc. That is all very useful for humans writing code, even if a bit redundant on some technical level. But if an LLM is doing the work, none of that matters.
Are LLMs any good at generating rocq code?
I asked several LLMs on your behalf and they all said "yes". But they might be a little biased.
Why not put them to the test? It is only a prompt away. Rust is an available extraction target for Rocq, so you can even integrate it into your existing codebase.
>Why not put them to the test?
haha I shall. I like the idea of tighter constraints on LLM hence my enthusiasm for rust over python for vibecoding.
I did just try it and the first thing it did was try to download half a gig. Which is fine, except my fiber install is next week and I'm hotspotting off a phone. So that'll need to wait
...it did seem to fundamentally understand the ask though of "make me a plan to make a http hello world server".
Though at same time flagged that this isn't ideal
>Rocq/Coq is primarily for theorem proving; HTTP server implementation will be minimal
> Though at same time flagged that this isn't ideal
I suppose that depends how deep down the rabbit hole you want to go. HTTP is pretty minimal in and of itself. The complexity is due to it being layered on top of many other things, like TCP/IP, sockets, network devices, etc. Is it worth proving that your NIC functions according to spec? Probably not. But, if an HTTP server is what you are trying to build, like, parsing an HTTP request is quite suitable.
But a good case. I would suggest that Rocq is already proving itself. I expect by "make a http hello world server" you don't mean: First, invent the universe. Although maybe you do! Who knows? Your prompt is not clear. And since the type system is comprehensive enough to force you to actually think about what you really want, it is compelling you to be much more specific.
>I suppose that depends how deep down the rabbit hole you want to go.
I'm intellectually curious about whether a formal verification style vibecoding would work. It seems like the logical outcome of current trajectory - if compute increases exponentially then something where the LLM can just hammer away until it checks out seems ideal way of vibecoding while getting a bullet proof outcome.
Knowing absolutely nothing about formal verification I'm quite skeptical it's viable right now though. (For hobby projects, I'm sure the formal verification academics are having fun)
So still leaning towards rust as current optimal. I am ofc biased (python/rust is my preference depending on task).
>I expect by "make a http hello world server" you don't mean
There is no deeper thinking behind it. Selected it purely because if I ask a LLM to oneshot something without guidance I think keeping it simple and within training data is fair.
Python is at least as typed as Lua.
It's talking about Luau (gradually typed, https://luau.org/), not Lua.
Hopefully https://github.com/astral-sh/ty will make the Python typing situation better, but absent that, Python typing is... not great. Honestly even with that it feels subjectively very finicky.
icontract or pycontracts -like DbC Design-by-Contract type and constraint checking at runtime with or as fast as astral-sh/ty would make type annotations useful at runtime
"Support runtime checking" : https://github.com/astral-sh/ty/issues/867 :
> [ typeguard, beartype, trycast; mypyc ]
mypyc/mypyc: Compile type annotated Python to fast C extensions https://github.com/mypyc/mypyc src: https://github.com/python/mypy/tree/master/mypyc .. docs: https://mypyc.readthedocs.io/en/latest/ :
mypyc docs > Using type annotations > Strict runtime type checking: https://mypyc.readthedocs.io/en/latest/using_type_annotation... :
> Mypyc ensures type safety both statically and at runtime. [...] `Any` types and erased types in general can compromise type safety, and this is by design. Inserting strict runtime type checks for all possible values would be too expensive and against the goal of high performance.
Oh my!
beartype docs: https://beartype.readthedocs.io/en/latest/ :
> Welcome to the Bearpedia
trycast: https://github.com/davidfstr/trycast :