I wonder why he didnt just start writing high-assurance software in a lightweight formalism or working with proof assistants. I saw him do a piece on Hoare triplets or something. A formal semantics or verifying popular libraries in Rust might have satisfied his need for math and correctness while getting something done.
My personal Rust verification project is to verify str::contains in the standard library. It is quite challenging, as it uses two-way substring search algorithm, and as far as I can tell there is no verified implementation of this algorithm in any system.
Something that’s a first, but still smallish, sounds like a great project to tackle. Good luck. Do post a write up once you get it done.
Or it would contribute to the feeling of vaporware that nobody uses. That is not meant as being critical of proofs, just that the field seems even more prone to the problems of lots of work that nobody is yet using, and he is getting no benefit from.
That’s true. He’d have to use it on something that doesn’t change often that he can drop into existing stack. Good example is verified crypto that miTLS is dropping into Firefox. Other possibilities Ive seen people prototype were string libraries, GMP, and C libraries (ie stdlib). Plenty potential fo do verified stuff people will use.
I agree with him. To be honest, the risk reward for such ambitious projects does not make sense. Years of effort to write a new filesystem, and for what gain? That level of effort and talent could be spent on numerous other things that would work out better for both the world and the author.
Most OSS is subsidized in two ways by companies, unsatisfied workers with a feeling they must do something else, and paying engineers enough so they don’t go broke while wasting massive amounts of time on some questionable projects. I hope the career in mathematics makes him/her happy.
If you don’t find the hobby work you do rewarding, then for sure stop doing it. I fiddle with my projects because I enjoy the fiddling, and try to not do so for any other reason.