In this day and age, it’s probably best to understand that blindly suggesting something should be in Rust is indistinguishable from zealotry. Or from mockery of the people who do it.

A better question to ask would have been, why settle for just memory safety - does a formally verified sshd exist? That kind of thing seems to be implemented more in OCaml and F#, like Project Everest, which has formally verified implementations of primitives (HACL) TLS, QUIC, and Signal https://project-everest.github.io/ ... ssh is notably missing?

I had a dig and found that ssh had in fact been done 9 years ago, tho it doesn't seem to have made it to a distribution: it's an offshoot of the CryptoVerif project[1] (which is, maybe unsurprisingly, under the umbrella of the same Prosecco team at Inria who worked on Project Everest). In 2015 Bruno Blanchet and David Cadé wrote a paper "From Computationally-Proved Protocol Specifications to Implementations and Application to SSH"[2] which describes using CryptoVerif to generate an implementation of SSH from the spec; the code is in the CryptoVerif tarball, but someone's helpfully put that up on github if you want a look[3]

The eye opening bits in the paper (given the claims of tinyssh to be small at < 100k words): "We have verified that our client and server correctly interoperate with OpenSSH...in order to give an idea on the amount of code this work represents, the CryptoVerif specification amounts to 331 lines of code, and we generate from it 531 lines of OCaml, split among multiple files. The manually written code representing the primitives and the authentication and connection protocols amount to 1124 lines."

The bad news would be that it's not very performant: 30MB/s compared to 90MB/s for openssh on the same hardware, in the paper. Since HACL is from the same stable and was designed to perform well as well as be verified, it might be worth dusting off and seeing if this could be made more usable. The implementation probably has value even if just as a test oracle.

[1]: https://bblanche.gitlabpages.inria.fr/CryptoVerif/

[2]: https://bblanche.gitlabpages.inria.fr/publications/CadeBlanc...

[3]: https://github.com/mgrabovsky/cryptoverif/tree/master/implem... the official implementation appears to be here now https://gitlab.inria.fr/bblanche/CryptoVerif/-/tree/master/c...

Can you justify this further in the context of this specific offering which appears not to manage dynamic memory?

This kind of comment had become a joke these days, especially when you say that under a project written in C. Nobody is going to even think about that until Rust has as good portability as C.

I feel like someone has to say this:

What about LISP?!

Excellent point; which production-grade rust ssh server would you recommend?