4 ms·

You're right that you can't define a safe subset of C without making it impractical. MISRA C defines a C subset intended to help avoid C's footguns, but it stil

You're right that you can't define a safe subset of C without making it impractical. MISRA C defines a C subset intended to help avoid C's footguns, but it still isn't actually a safe language. There are alternative approaches though: 1. Compile a safe language to C (whether a new language or an existing one) 2. Formal analysis of C, or of some practical subset of C, to prove the absence of undefined behaviour Work has been done on both approaches. ZZ compiles to C. [0] Dafny can compile to C++, but it seems that's not its primary target. [1][2] There are several projects on formal analysis of C. [3][4][5][6] [0] https://github.com/zetzit/zz https://github.com/zetzit/zz [1] https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny [2] https://dafny-lang.github.io/dafny/ https://dafny-lang.github.io/dafny/ [3] https://frama-c.com/ https://frama-c.com/ [4] https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/ https://www.microsoft.com/en-us/research/project/vcc-a-verif... [5] https://www.eschertech.com/products/ecv.php https://www.eschertech.com/products/ecv.php [6] https://trust-in-soft.com/ https://trust-in-soft.com/

geofft 5y ago
Is it better to write ZZ or Dafny code than to write Java, Python, Haskell, Rust, or Swift code? (They look cool and I'm enjoying reading about them, but for the things I do for my day job where C is one of the obvious options, I'm not sure they're better options, but usually one of the languages above is a better option.)
- MaxBarraclough 5y ago
  ZZ's whole goal is to transpile to C, which (as their website mentions) has some practical advantages. Consider exotic hardware platforms where there's a vendor-provided proprietary C compiler and no other choice. Dafny has a slightly different emphasis, as it's about formal verification, so it's more competing with Ada SPARK than with mainstream languages. I can't comment on the general ergonomics on ZZ and Dafny as I've not tried them out, but presumably they're going to be well behind a language like Java with its huge ecosystem of IDEs etc. Neither seems particularly mature, either, so I wouldn't bet the farm on them. > Is it better to write ZZ or Dafny code than to write Java, Python, Haskell, Rust, or Swift code? If you've got the choice and you're just trying to do 'normal day job programming' I imagine that yes you'd be much better off just using Java. If you want a language that's quite like C or C++ but much better regarding safety, there are Rust, Zig, and the too-often-overlooked Ada language.

geofft 5y ago

Is it better to write ZZ or Dafny code than to write Java, Python, Haskell, Rust, or Swift code? (They look cool and I'm enjoying reading about them, but for the things I do for my day job where C is one of the obvious options, I'm not sure they're better options, but usually one of the languages above is a better option.)

MaxBarraclough 5y ago
ZZ's whole goal is to transpile to C, which (as their website mentions) has some practical advantages. Consider exotic hardware platforms where there's a vendor-provided proprietary C compiler and no other choice. Dafny has a slightly different emphasis, as it's about formal verification, so it's more competing with Ada SPARK than with mainstream languages. I can't comment on the general ergonomics on ZZ and Dafny as I've not tried them out, but presumably they're going to be well behind a language like Java with its huge ecosystem of IDEs etc. Neither seems particularly mature, either, so I wouldn't bet the farm on them. > Is it better to write ZZ or Dafny code than to write Java, Python, Haskell, Rust, or Swift code? If you've got the choice and you're just trying to do 'normal day job programming' I imagine that yes you'd be much better off just using Java. If you want a language that's quite like C or C++ but much better regarding safety, there are Rust, Zig, and the too-often-overlooked Ada language.