Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

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


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 :)


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


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




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: