5 ms·

All of Windows (including the NT kernel) is written using the same basic proof model that Wuffs uses, except that the constraints are specified as annotations o

All of Windows (including the NT kernel) is written using the same basic proof model that Wuffs uses, except that the constraints are specified as annotations on top of C and C++ instead of as a new programming language. I prefer the annotation approach, TBH, but I'm glad to see people working on safety. Specifically, Wuffs (like Rust) has this problem where it tries to fill the same niche as C and C++ and improve on these older languages in specific ways, but in addition to being different in ways necessary to achieve the language's objective is also different from C and C++ in totally gratuitous ways that are basically just aesthetic differences --- for example, "type var" vs "var: type". I'm a big believer in technical continuity. IMHO, a lot of recent language developments should have instead been extensions of C, C++, Java, or Python.

amelius 6y ago
But the C++ spec has become quite unwieldy, so I can understand the desire to start a totally new language.
- edflsafoiewq 6y ago
  The previous post on the blog has an observation that applies to languages as well > Software has a Peter Principle. If a piece of code is comprehensible, someone will extend it, so they can apply it to their own problem. If it’s incomprehensible, they’ll write their own code instead. Code tends to be extended to its level of incomprehensibility.
matu3ba 6y ago
What tool/framework do they use for annotation and are there standards like SMTlib2, but for annotating those kind of things? Can this tools verify that the annotations are correct wrt the code below or above?
- quotemstr 6y ago
  https://docs.microsoft.com/en-us/cpp/code-quality/understanding-sal?view=msvc-160 https://docs.microsoft.com/en-us/cpp/code-quality/understand...
remexre 6y ago
I work on (well, mostly near) an extensible C compiler, designed so extension authors can independently create extensions, and users can import them as easily as libraries: https://github.com/melt-umn/ableC/ https://github.com/melt-umn/ableC/ (and I'd love to answer any questions you have about our approach or code.) IMO this approach hasn't taken off because maintaining compatibility with C while adding safety (or really just about any property) means implementing your own sublanguage that can't arbitrarily call C functions while maintaining your safety properties. On the other hand, C being able to call into your sublanguage easier is a benefit versus jury-rigging Cargo into your build system (in the case of Rust). On the other hand, this approach works great for adding extensions that increase the expressive power of C with new abstractions, for example algebraic data types, C++-like templating, etc.
kbenson 6y ago
> I'm a big believer in technical continuity. IMHO, a lot of recent language developments should have instead been extensions of C, C++, Java, or Python. If that's what you really wanted, and if we always did that, then you would probably want extensions to Perl instead of Python, since it predated it slightly and was much more popular much earlier. Instead, I think what you're really asking for is language extensions to the things you are familiar with. Those happen to be things a lot of other people are also familiar with, but that doesn't change that the same strategy results in Perl still getting the lion's share of attention. I, for one, would be perfectly happy with that, as I love Perl, but many people would not, and possibly not for any real technical reason. Anyone that thinks the case for Rust or D is better served by extensions to C or C++ but thinks that Python is objectively a better language than Perl should probably look deeply at exactly why they hold those views. P.S. That's not really to say you hold those views. Consider this comment less a critique of your specific statement than slight tangent spurred by it.
- pjmlp 6y ago
  Not the OP, but I do share the sentiment of improving existing unsafe languages. The C and C++ code in many relevant stacks is not going away, and many of us won't be ever be able to use D or Rust regardless of how much we like them. UNIX clones, Windows, .NET and Java runtime implementation, WinUI/WinRT, Android (regardless of this week's annoucement) So Microsoft Checked C, Microsoft SAL, Visual C++/clang/gcc lifetime analysers, Frama-C, hardware memory tagging, Pluton sandbox, CHERI,... are all welcomed improvements.
  - kbenson 6y ago
    Yes, I'm not against improving existing languages. I just don't think it's always sufficient, so we shouldn't accept the false dichotomy of improving existing languages or creating and promoting the use of new ones to take advantage of new ideas and technologies to their fullest. Even if Rust were to fully supplant C and C++ for at least systems programming[1], we should hope that within a few decades it's a risk of being supplanted by something else. To want otherwise is likely to inadvertently want stagnation and/or a language that while likely still improving, is having new technologies and concepts bolted on in increasingly convoluted manner, as they were not and could not have been considered when designing the language originally. 1: I think this is unlikely, if only because I don't see one language supplanting C, I see C's market cannibalized by a few different languages, with C always retaining some use.
WalterBright 6y ago
> I'm a big believer in technical continuity. So am I. D is designed to be an easy transition from C and C-With-Classes. For example, here is some code in C that was translated to D (it's part of the Digital Mars C++ compiler): C: https://github.com/DigitalMars/Compiler/blob/dmc-cxx/dm/src/dmc/divcoeff.c https://github.com/DigitalMars/Compiler/blob/dmc-cxx/dm/src/... D: https://github.com/DigitalMars/Compiler/blob/master/dm/src/dmc/divcoeff.d https://github.com/DigitalMars/Compiler/blob/master/dm/src/d... They look pretty much the same. The code generated is the same. In those repositories you can also see how I translated the C versions to D with plenty of examples. The biggest impediment is the C preprocessor. You wouldn't really want to carry that forward. After removing dependency on the C preprocessor, most of the work is global search/replacing things like `->` to `.`.
pjmlp 6y ago
As info for others, here are the annotations, https://docs.microsoft.com/en-us/cpp/code-quality/using-sal-annotations-to-reduce-c-cpp-code-defects?view=msvc-160 https://docs.microsoft.com/en-us/cpp/code-quality/using-sal-...

amelius 6y ago

But the C++ spec has become quite unwieldy, so I can understand the desire to start a totally new language.

edflsafoiewq 6y ago
The previous post on the blog has an observation that applies to languages as well > Software has a Peter Principle. If a piece of code is comprehensible, someone will extend it, so they can apply it to their own problem. If it’s incomprehensible, they’ll write their own code instead. Code tends to be extended to its level of incomprehensibility.

matu3ba 6y ago

What tool/framework do they use for annotation and are there standards like SMTlib2, but for annotating those kind of things? Can this tools verify that the annotations are correct wrt the code below or above?

quotemstr 6y ago
https://docs.microsoft.com/en-us/cpp/code-quality/understanding-sal?view=msvc-160 https://docs.microsoft.com/en-us/cpp/code-quality/understand...

remexre 6y ago

I work on (well, mostly near) an extensible C compiler, designed so extension authors can independently create extensions, and users can import them as easily as libraries: https://github.com/melt-umn/ableC/ https://github.com/melt-umn/ableC/ (and I'd love to answer any questions you have about our approach or code.) IMO this approach hasn't taken off because maintaining compatibility with C while adding safety (or really just about any property) means implementing your own sublanguage that can't arbitrarily call C functions while maintaining your safety properties. On the other hand, C being able to call into your sublanguage easier is a benefit versus jury-rigging Cargo into your build system (in the case of Rust). On the other hand, this approach works great for adding extensions that increase the expressive power of C with new abstractions, for example algebraic data types, C++-like templating, etc.

kbenson 6y ago

> I'm a big believer in technical continuity. IMHO, a lot of recent language developments should have instead been extensions of C, C++, Java, or Python. If that's what you really wanted, and if we always did that, then you would probably want extensions to Perl instead of Python, since it predated it slightly and was much more popular much earlier. Instead, I think what you're really asking for is language extensions to the things you are familiar with. Those happen to be things a lot of other people are also familiar with, but that doesn't change that the same strategy results in Perl still getting the lion's share of attention. I, for one, would be perfectly happy with that, as I love Perl, but many people would not, and possibly not for any real technical reason. Anyone that thinks the case for Rust or D is better served by extensions to C or C++ but thinks that Python is objectively a better language than Perl should probably look deeply at exactly why they hold those views. P.S. That's not really to say you hold those views. Consider this comment less a critique of your specific statement than slight tangent spurred by it.

pjmlp 6y ago
Not the OP, but I do share the sentiment of improving existing unsafe languages. The C and C++ code in many relevant stacks is not going away, and many of us won't be ever be able to use D or Rust regardless of how much we like them. UNIX clones, Windows, .NET and Java runtime implementation, WinUI/WinRT, Android (regardless of this week's annoucement) So Microsoft Checked C, Microsoft SAL, Visual C++/clang/gcc lifetime analysers, Frama-C, hardware memory tagging, Pluton sandbox, CHERI,... are all welcomed improvements.
- kbenson 6y ago
  Yes, I'm not against improving existing languages. I just don't think it's always sufficient, so we shouldn't accept the false dichotomy of improving existing languages or creating and promoting the use of new ones to take advantage of new ideas and technologies to their fullest. Even if Rust were to fully supplant C and C++ for at least systems programming[1], we should hope that within a few decades it's a risk of being supplanted by something else. To want otherwise is likely to inadvertently want stagnation and/or a language that while likely still improving, is having new technologies and concepts bolted on in increasingly convoluted manner, as they were not and could not have been considered when designing the language originally. 1: I think this is unlikely, if only because I don't see one language supplanting C, I see C's market cannibalized by a few different languages, with C always retaining some use.

WalterBright 6y ago

> I'm a big believer in technical continuity. So am I. D is designed to be an easy transition from C and C-With-Classes. For example, here is some code in C that was translated to D (it's part of the Digital Mars C++ compiler): C: https://github.com/DigitalMars/Compiler/blob/dmc-cxx/dm/src/dmc/divcoeff.c https://github.com/DigitalMars/Compiler/blob/dmc-cxx/dm/src/... D: https://github.com/DigitalMars/Compiler/blob/master/dm/src/dmc/divcoeff.d https://github.com/DigitalMars/Compiler/blob/master/dm/src/d... They look pretty much the same. The code generated is the same. In those repositories you can also see how I translated the C versions to D with plenty of examples. The biggest impediment is the C preprocessor. You wouldn't really want to carry that forward. After removing dependency on the C preprocessor, most of the work is global search/replacing things like `->` to `.`.

pjmlp 6y ago

As info for others, here are the annotations, https://docs.microsoft.com/en-us/cpp/code-quality/using-sal-annotations-to-reduce-c-cpp-code-defects?view=msvc-160 https://docs.microsoft.com/en-us/cpp/code-quality/using-sal-...