4 ms·
My understanding is that the key feature of SPARK is design-by-contract aka run-time enforced pre- and post-conditions plus invariants for loops. Whereas F* let
by letmeinhere 2y ago
My understanding is that the key feature of SPARK is design-by-contract aka run-time enforced pre- and post-conditions plus invariants for loops. Whereas F* lets you define dependendent types, a subset of which are compile-time constraints similar to those SPARK contracts. Is that a fair contrast?
- Jtsummers 2y agoFairly short course on SPARK/Ada - https://learn.adacore.com/courses/intro-to-spark/index.html https://learn.adacore.com/courses/intro-to-spark/index.html SPARK's pre-/postconditions and assertions can be statically checked, they aren't just for runtime enforcement. This is its key value proposition, if it were just runtime enforcement it'd be nice, but not that great.