[irundebian]

It can be a binary property if you define security as a proof of absence of runtime errors which is possible to achieve today.

[saagarjha]

This isn’t really possible to achieve.

[irundebian]

It's possible. You can prove absence of runtime errors with Ada/SPARK (which is using theorem provers).