Comment by bneb-dev
5 days ago
SPARK seems interesting. Any ideas how it compares to Salt?
- C performance? - Generics? - Syntax ergonomics?
Thanks for sharing!
5 days ago
SPARK seems interesting. Any ideas how it compares to Salt?
- C performance? - Generics? - Syntax ergonomics?
Thanks for sharing!
Yes, it has generics. The syntax is Pascal-like, which some people used to C-family languages dislike but I personally find nice. Performance can definitely match performant C code. (intended use cases include real-time systems and embedded devices)
The language overview can be found here: https://docs.adacore.com/spark2014-docs/html/ug/en/spark_201...
It is a way to formally verify Ada, it meets all those criterias.
It looks like verification is distinct from the compiler.