[OliverM]

Are there proofs for other languages/runtimes available? I'd love to see the level of rigour needed to demonstrate that

[WJW]

One thing I know of is the CoPilot language/library/thingy from NASA (no relation to Githubs copilot), which can takes in code in a Haskell DSL and outputs code that is guaranteed to run in constant memory and uses an equal number of cycles each loop. See it here: https://copilot-language.github.io/

Also if you ever find yourself needing to write hard real-time code for your arduino, check out my blog post about the arduino-copilot library at https://wjwh.eu/posts/2020-01-30-arduino-copilot.html :)

[OliverM]

Thank you, your blog post was a pleasure to read. CoPilot looks great!

[Ono-Sendai]

My programming language Winter has bounded memory and space usage: https://github.com/glaretechnologies/winter, for at least a subset of the language.