#sparetimeproject — Public Fediverse posts

To my surprise, the idea I had last night is actually working just fine in #RustLang.

So, my #VisualNovel #SpareTimeProject is now probably going to use an #eDSL encoded as a #FreeMonad which is wrapped in a #StateMonadTransformer.

Now I just need to continue working on it. I haven't made much progress in the last 9 months...

Tonight I had strange dreams about state monads...

I currently have some waiting time at work, and am now trying to change some things in my #RustLang #SpareTimeProject, as I would like to try using a State Monad Transformer together with a Free Monad. I don't think that this combination is going to work for what I am trying to achieve, but after tonight I just have to try it.

And I must say, I already miss the #Lean4 Syntax. Rust is just sooooo verbose when it comes to nested generics...

After simplifying the get-function in my current #SpareTimeProject (a formally validated heap), I had to make a lot of changes as #Lean4 fails to unfold the new function definition.

However, I am very happy with the results. The inability to unfold forced me to rewrite some proofs in the formal validation, now using hand-written lemmas instead of unfolding the function definition. The new code is about 200 lines shorter than the old one, easier to read, and more robust.

https://github.com/soulsource/BinaryHeap/commit/b1821bdf7fb928be27a9919f4969883a2f6670ff

A few months ago a coworker made the prediction, that once I got to know #Lean4, I would port my #SpareTimeProject over from #RustLang.

I must say, he was not wrong... I would be so tempted. Lean feels way better suited for writing a #VisualNovel Engine than Rust. However, I have already done so much Rust-specific work, that I think I will manage to resist the urge of switching language, and finish this project in Rust.