On: Rust support in the Linux kernel

[rp1]

What advantages does Ada have over Rust (in terms of memory safety)?

[rcxdude → rp1]

Ada/SPARK allows formal verification of many more properties than just memory safety. Ada on its own does not have the same kind of memory safety guarantees as rust though.

[Quekid5 → rcxdude]

(I have no horse in this race, just curious.)

Are there any non-proprietary implementations of Ada/SPARK which don't place limitations on the compiler output?

[MaxBarraclough → Quekid5]

Apparently [0][1] the FSF distribution of GNAT permits development of non-GPL software.

[0] https://news.ycombinator.com/item?id=24492653

[1] https://old.reddit.com/r/ada/comments/3989f4/gnat_gpl_restri...

[Quekid5 → MaxBarraclough]

I was asking the opposite question, I think. I know of GNAT, but I was asking whether there's any Ada/Spark that has a GPL (or whatever non-proprietary) license.