5 ms·
Are there proofs for other languages/runtimes available? I'd love to see the level of rigour needed to demonstrate that
by OliverM 4y ago
Are there proofs for other languages/runtimes available? I'd love to see the level of rigour needed to demonstrate that
- WJW 4y agoOne 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/ 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 https://wjwh.eu/posts/2020-01-30-arduino-copilot.html :)
- OliverM 4y agoThank you, your blog post was a pleasure to read. CoPilot looks great!
- Ono-Sendai 4y agoMy programming language Winter has bounded memory and space usage: https://github.com/glaretechnologies/winter https://github.com/glaretechnologies/winter, for at least a subset of the language.