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.
> Knowing absolutely nothing about formal verification
Are you sure about that? That is what we've been talking about all along. After all, the thing that separates Rust from Python, with respect to our discussion here — the thing that allows code to be less fragile, is its type system. Which is formal verification! Rust is very limited in that regard, not allowing verification of much, but still very much lives on the formal verification spectrum.
The trouble when you can't verify much is that you end up in a situation where something like:
fn add(a: i32, b: i32) -> i32 {
a + b + 1
}
Is able to compile just fine despite being completely wrong. To deal with that you need to write tests (which is essentially runtime formal verification). But once you've written the tests, you've also largely covered the properties that are statically verified, leaving no real benefit to LLMs.
But I infer that you aren't writing tests either, and that Rust's type system is feeling advantageous as it at least provides some limited verification. You seem to be enjoying that workflow, which is why I mentioned that there are languages with way better types systems that you might enjoy even more. There are probably hundreds of languages between Rust and full verification on the spectrum, so if Rocq isn't the exact one for you, try some others! They're only a prompt away.
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