There are proof checkers. I'm not familiar with them though. I believe Coq does something similar.
Could you do this for an interpreted language? Sure, but strongly typed, functionally pure languages are generally compiled. (if I'm not mistaken, you'd be losing out on a virtually free speedup by not compiling).
Agda and Coq are both languages that also forbid infinite loops and thus have type systems that allow you to prove logical statements (via the Curry-Howard correspondence) about your programs.
It is cool to know your program has certain properties for all inputs by proving it, but also very time consuming :)
For further actions, you may consider blocking this person and/or reporting abuse
We're a place where coders share, stay up-to-date and grow their careers.
I laughed hard!
Do you need a compiler to do this, or can it be done with a separate program where no compiler exists for the language?
There are proof checkers. I'm not familiar with them though. I believe Coq does something similar.
Could you do this for an interpreted language? Sure, but strongly typed, functionally pure languages are generally compiled. (if I'm not mistaken, you'd be losing out on a virtually free speedup by not compiling).
Agda and Coq are both languages that also forbid infinite loops and thus have type systems that allow you to prove logical statements (via the Curry-Howard correspondence) about your programs.
It is cool to know your program has certain properties for all inputs by proving it, but also very time consuming :)