3 ms·
While I'm not sure this fits with Rust's existing concepts of safety and correctness, it would be interesting (and not just for RT purposes) to have a language
by 0xcde4c3db 11y ago
While I'm not sure this fits with Rust's existing concepts of safety and correctness, it would be interesting (and not just for RT purposes) to have a language in which one could mark functions as <= some complexity (given the usual simplifying assumptions) or provably terminating, and have the compiler throw an error if it can't prove that those constraints are met. Does something like this exist?
- abiox 11y agoi don't know, but wow, that's a really cool idea.
- Rusky 11y agoThe closest thing that comes to mind is total functional languages- the compiler doesn't deal with complexity classes, but it does prove termination. It's mostly used in dependently-typed languages and theorem provers so they can prove the type checker will terminate.