search

alshdavid / BorrowScript

TypeScript with a Borrow Checker. Multi-threaded, Tiny binaries. No GC. Easy to write.
1.45k stars 16 forks source link

Investigate forcing loops to have a well defined exit condition to allow for more powerful static analysis #33

Closed Isaac-Leonard closed 1 year ago

Isaac-Leonard commented 3 years ago

Some languages such as Alanlang and some C coding standards such as those used at JPL NASA enforce that any looping code has a well defined exit condition for loops to enable more powerful static analysis. While possibly overly strict This seems like it would be a useful feature for borrowScript to have although it would need to be well implemented to not limit dinamicness too much. These languages and standards also generally limit the depth of recursion however I believe that enforcing that cleanly would be harder as programmers would have to keep track of how far down the recursion stack they were as to not cause an error. Also this technically already exists in V8 and Firefox javascript engines as they haven't implemented tail call optimisation yet although that doesn't really count.

SuperSonicHub1 commented 3 years ago

What do you mean by this? Something like C's noreturn macro?

Isaac-Leonard commented 3 years ago

Not exactly no although that does sound useful. This mainly focuses on the ability to parallelise however is still relevant to static analysis: https://alan-lang.org/the-turing-completeness-problem.html Heres the nasa coding standards I was referencing too: https://en.wikipedia.org/wiki/The_Power_of_10:_Rules_for_Developing_Safety-Critical_Code#Rules The main ones I'm thinking about here are the first two.

SuperSonicHub1 commented 3 years ago

Oh, OK. So we want to make sure that BorrowScript disincentives use of labels, recursion, etc.? We could just not include labels in our TypeScript subset and have a small stack limit. Perhaps this would be a compiler option?

On Sat, Oct 23, 2021, 6:05 PM Isaac-Leonard @.***> wrote:

Not exactly no although that does sound useful. This mainly focuses on the ability to parallelise however is still relevant to static analysis: https://alan-lang.org/the-turing-completeness-problem.html Heres the nasa coding standards I was referencing too:

https://en.wikipedia.org/wiki/The_Power_of_10:_Rules_for_Developing_Safety-Critical_Code#Rules The main ones I'm thinking about here are the first two.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/alshdavid/BorrowScript/issues/33#issuecomment-950224145, or unsubscribe https://github.com/notifications/unsubscribe-auth/AGDQCMSM7EU65PUAI2X2WKTUIMWSXANCNFSM5GR5XF7Q .

Isaac-Leonard commented 3 years ago

Not exactly. The point would be for it to be analysed at compile time, so the program doesn't get into any unexpected infinite loops.