43 ms·

Checked C

264 points by soheilpro 4y ago

timmg 4y ago
Quite honestly, I love what MS has done with JavsScript with Typescript. It would be great if they could do the same for C. I guess the hard part will be the fact that all your dependent libraries will (likely) still be unsafe.
- pjmlp 4y ago
  See also https://devblogs.microsoft.com/cppblog/high-confidence-lifetime-checks-in-visual-studio-version-17-5-preview-2/ https://devblogs.microsoft.com/cppblog/high-confidence-lifet...
  - flohofwoe 4y ago
    I'm a bit confused, at the start they talk about C++, but some of the code examples look like C. Do those checks also work in the C compiler? (the difference is kinda important, because unlike Clang, the MSVC C++ compiler doesn't have enough non-standard language extensions to compile C code that was written in the last 20 years).
    - pjmlp 4y ago
      They talk about C++, because that is what mostly matters to Visual C++ customers, however /analyse mode also works in C code. https://learn.microsoft.com/en-us/cpp/code-quality/code-analysis-for-c-cpp-overview?view=msvc-170 https://learn.microsoft.com/en-us/cpp/code-quality/code-anal...
      - sendfoods 4y ago
        I'm a bit confused. Didn't Herb Sutter essentially fork clang and extended the codebase in the beginning? Is microsoft working with that fork and (most importantly) re-contributing?
        pjmlp 4y ago
        If you mean cpp2, that has nothing to do with Microsoft, it's Herb's personal project.
        sendfoods 4y ago
        No, his lifetime work, e.g. https://herbsutter.com/2018/09/20/lifetime-profile-v1-0-posted/ https://herbsutter.com/2018/09/20/lifetime-profile-v1-0-post...
        pjmlp 4y ago
        No that was a proof of concept for a paper that went nowhere. VC++ analysis builds up on SAL infrastructure. https://learn.microsoft.com/en-us/cpp/code-quality/understanding-sal?view=msvc-170 https://learn.microsoft.com/en-us/cpp/code-quality/understan... "Closing the Gap between Rust and C++ Using Principles of Static Analysis - CppCon 2020" https://www.youtube.com/watch?v=_pQGRr4P16w https://www.youtube.com/watch?v=_pQGRr4P16w There is also a clang work on lifetimes, but little progress has happened since 2019. "Lifetime analysis for everyone - CppCon 2019" https://www.youtube.com/watch?v=d67kfSnhbpA https://www.youtube.com/watch?v=d67kfSnhbpA
        sendfoods 4y ago
        SAL, as I understand it, is Visual Studio/Microsoft only? Do you have any idea if this work will make it to clang/gcc/g++?
        int_19h 4y ago
        SAL is deliberately designed such that it can be defined as a bunch of macros that expand to whatever compiler-specific magic the implementation needs (e.g. MSYS64 doesn't support it at all, but they define all those macros as no-op, so code still compiles). So in principle it could work across implementations.
- phailhaus 4y ago
  I'm begging them to do the same for Python.
  - corndoge 4y ago
    They made pyright which is pretty rad
    - phailhaus 4y ago
      Yeah it's pretty great, but still hamstrung by the inherent limitations of the language itself. Would love to see a new language on top of Python that treats types as first-class constructs.
      - still_grokking 4y ago
        Why "on top of Python"? The runtime is slow as hell, limited and actually very aged. But there are better modern alternatives. https://docs.scala-lang.org/scala3/book/scala-for-python-devs.html https://docs.scala-lang.org/scala3/book/scala-for-python-dev... Types in Scala are not only "first-class". You can even program with them like in TS. https://blog.rockthejvm.com/type-level-programming-scala-3/ https://blog.rockthejvm.com/type-level-programming-scala-3/ (Type level functions are correctness proves, BTW.) Enjoy!
        still_grokking 4y ago
        I guess I should have mentioned that Scala 3, with its new syntax, look almost like "Python with types". That's why I've mentioned it.
pjmlp 4y ago
Older discussions on Checked C, https://news.ycombinator.com/item?id=30321535 https://news.ycombinator.com/item?id=30321535 https://news.ycombinator.com/item?id=19424106 https://news.ycombinator.com/item?id=19424106
belter 4y ago
"A Formal Model of Checked C" - https://news.ycombinator.com/item?id=30321535 https://news.ycombinator.com/item?id=30321535 - 37 comments - 10 months ago "Checked C" - https://news.ycombinator.com/item?id=26190403 https://news.ycombinator.com/item?id=26190403 - 133 comments - 2021 "Refactoring the FreeBSD Kernel with Checked C" - https://news.ycombinator.com/item?id=25989115 https://news.ycombinator.com/item?id=25989115 - 41 comments - 2021 "Achieving Safety Incrementally with Checked C" - https://news.ycombinator.com/item?id=19424106 https://news.ycombinator.com/item?id=19424106 - 21 comments - 2019 "Checked C: Making C Safer by Extension" - https://news.ycombinator.com/item?id=17939537 https://news.ycombinator.com/item?id=17939537 - 55 comments - 2018 "Checked C: extension to C that adds static and dynamic checking" - https://news.ycombinator.com/item?id=16588483 https://news.ycombinator.com/item?id=16588483 - 92 comments - 2018 "Checked C" - https://news.ycombinator.com/item?id=11899925 https://news.ycombinator.com/item?id=11899925 - 156 comments - 2016
- dang 4y ago
  Thanks! Added a few: C to Checked C by 3C - https://news.ycombinator.com/item?id=30857289 https://news.ycombinator.com/item?id=30857289 - March 2022 (1 comment) A Formal Model of Checked C - https://news.ycombinator.com/item?id=30321535 https://news.ycombinator.com/item?id=30321535 - Feb 2022 (37 comments) Why Checked C when there was Verona? - https://news.ycombinator.com/item?id=26499846 https://news.ycombinator.com/item?id=26499846 - March 2021 (2 comments) Checked C - https://news.ycombinator.com/item?id=26190403 https://news.ycombinator.com/item?id=26190403 - Feb 2021 (133 comments) Refactoring the FreeBSD Kernel with Checked C [pdf] - https://news.ycombinator.com/item?id=25989115 https://news.ycombinator.com/item?id=25989115 - Feb 2021 (41 comments) Refactoring the FreeBSD Kernel with Checked C [pdf] - https://news.ycombinator.com/item?id=24019185 https://news.ycombinator.com/item?id=24019185 - Aug 2020 (13 comments) Achieving Safety Incrementally with Checked C - https://news.ycombinator.com/item?id=19424106 https://news.ycombinator.com/item?id=19424106 - March 2019 (21 comments) Checked C: Making C Safer by Extension - https://news.ycombinator.com/item?id=17939537 https://news.ycombinator.com/item?id=17939537 - Sept 2018 (55 comments) Checked C: extension to C that adds static and dynamic checking - https://news.ycombinator.com/item?id=16588483 https://news.ycombinator.com/item?id=16588483 - March 2018 (92 comments) Checked C - https://news.ycombinator.com/item?id=12049548 https://news.ycombinator.com/item?id=12049548 - July 2016 (3 comments) Checked C – A Safer C/C++ from Microsoft - https://news.ycombinator.com/item?id=11936418 https://news.ycombinator.com/item?id=11936418 - June 2016 (3 comments) Checked C - https://news.ycombinator.com/item?id=11899925 https://news.ycombinator.com/item?id=11899925 - June 2016 (156 comments)
WalterBright 4y ago
Checked C: int a[5] = { 0, 1, 2, 3, 4}; _Array_ptr<int> p : count(5) = a; // p points to 5 elements. My proposal for C: int a[5] = { 0, 1, 2, 3, 4}; int p[..] = a; // p points to 5 elements. https://www.digitalmars.com/articles/C-biggest-mistake.html https://www.digitalmars.com/articles/C-biggest-mistake.html https://github.com/Microsoft/checkedc/wiki/New-pointer-and-array-types#checked-single-dimensional-arrays https://github.com/Microsoft/checkedc/wiki/New-pointer-and-a...
- KingLancelot 4y ago
  Fat pointers are a good idea, but I think it’d be a better idea to store the start and evd pointers instead of a pointer to the first element and a size_t.
  - 1980phipsi 4y ago
    Why?
    - masklinn 4y ago
      I'd guess it's because that's what C++ does. Though it's unclear to me that C++-style iteration (where you increment a running pointer until you reach an EOI pointer) is much used in C.
      - WalterBright 4y ago
        Storing two pointers into the same array is a memory safety problem. It's hard to implement a borrow checker when there are two live mutable pointers into the same memory object.
        int_19h 4y ago
        I would expect the borrow checker to treat a slice as a logical pointer to all elements that are addressable through it, regardless of how it's implemented under the hood.
jimbob45 4y ago
Why not just use C++? Also why can we not get better syntax for C? Function pointer syntax is so bad that people actively avoid using them. #pragma once is a hack. Every string library function is actively dangerous in addition to puts/gets. I know that nobody wants to be the one to mess with the core language and ruin it but this is awfully low-hanging fruit that hasn’t been fixed in 50 years.
- mirekrusin 4y ago
  It has been fixed. The fix has the codename "zig".
  - shrimp_emoji 4y ago
    I heard it was "Rust".
    - chaosite 4y ago
      Rust is more comparable to C++ than C.
    - anfilt 4y ago
      Rust is not exactly a C replacement. Definitely the better choice these days over C++ in my opinion if you can use rust. It can be made to function more like C with #![no_std]. However that is an even less than batteries included experience than C.
      - masklinn 4y ago
        > Rust is not exactly a C replacement. Rust is absolutely a C replacement. Whether C heads want to use it is a more complicated question. But some are very much into it (e.g. Brian Cantrill). > It can be made to function more like C with #![no_std]. However that is an even less than batteries included experience than C. std assumes you have a heap and IO, which most C environments do. no_std removes all that (leaving only libcore as baseline), however you can re-add a dependency on "alloc" to get allocations and most of the standard collections back (all but hashset and hashmap, because no secure RNG). You can also / instead fill your needs with third-party crates more dedicated to restricted or freestanding environments, like heapless (https://crates.io/crates/heapless https://crates.io/crates/heapless).
gavinray 4y ago
Note that active development seems to be continuing here: https://github.com/secure-sw-dev/checkedc-llvm-project https://github.com/secure-sw-dev/checkedc-llvm-project
kelnos 4y ago
Thinking about this at a higher level, the real problem is that we use C arrays at all. But we can't stop using C arrays, because libc and a huge body of other C libraries out there represent lists of data using C arrays. As a useful counterexample, glib has GArray, GPtrArray, and GList, along with functions that you use to manipulate the lists. Those functions are presumably implemented correctly, and will prevent you from making out-of-bounds accesses. But of course those things are not widely adopted, because they're not standardized, they're not in libc, and libc has not been reimagined such that all of its APIs take and return these safer list primitives instead of bare C arrays. (And sure, GArray etc. are not necessarily suitable everywhere, as they require heap allocations. But I could imagine a safe abstraction that could allow for using stack or static allocations to back it.) So I see something like Checked C as a band-aid, when the language and stdlib just needs a complete overhaul. Obviously that's incredibly unlikely to ever happen, so something like Checked C is a decent compromise, I guess.
- sramsay 4y ago
  > As a useful counterexample, glib has GArray, GPtrArray, and GList, along with functions that you use to manipulate the lists. Those functions are presumably implemented correctly, and will prevent you from making out-of-bounds accesses. > But of course those things are not widely adopted, because they're not standardized, they're not in libc, and libc has not been reimagined such that all of its APIs take and return these safer list primitives instead of bare C arrays. I'm really not sure why the second thing is regarded by C programmers as such an insuperable barrier to the first thing. I absolutely understand that there are circumstances where extreme portability is a major requirement. That, and C's ability to operate in highly constrained environments are among its most laudable features. But many of us (including me) write user-facing C applications that have neither requirement and where Glib is either already installed or easy to install. Why not just go ahead and use it? If you're trying to get it to run on a tiny embedded system or in some land without Glib . . . well, this isn't the program for you! I feel like this is more of a weird cultural prejudice than a technical matter. People run programs in JavaScript (or Haskell, or Python) with hundreds of dependencies, and while some find that annoying, I don't hear people in these communities objecting to idea of dependencies the way people do with C. Could the standard library be better? Of course. But there's something to be said for not including a lot of batteries in the standard and just using the third-party tools that are available.
nottorp 4y ago
Hmm. Didn't Turbo Pascal have array bounds checking 3 billion years ago when we all had pet dinosaurs? It could have simply been added to the compiler in C as well...
- baq 4y ago
  Turbo Pascal had a lot of good ideas back in the late 80s and early 90s which were ridiculed back then and are now considered best practices… modules, safe strings, safe arrays, Delphi added quite nice objects. Alas, it was never popular in the Internet age. Just imagine if we had pascalscript instead of JavaScript - a decade of wasted developer time saved…
  - tored 4y ago
    Correct me if I’m wrong but didn’t a few BASIC dialects, like QuickBasic and Turbo Basic, also support that back then? Truly bizarre that we ended up with C, still feature incomplete compared to what was available at the time.
    - 0xbadcafebee 4y ago
      The history of technology is littered with examples of a technically superior solution being abandoned for a crappier solution.
    - pjmlp 4y ago
      All major systems programming languages starting with JOVIAL in 1958, had bounds checking. ESPOL/NEWP from 1961, almost a decade before C came to be, even had unsafe code blocks!
  - Tozen 4y ago
    There are those that would argue that the reasons for Pascal being lesser known than it should, involve the machinations of AT&T, other corporate entities, and orchestrated negative media. Pascal was in the way of what they were trying to push. And if people look deeper, there are some surprising elements of Pascal in newer languages, more than many realize. At some point, sanity and common sense will sneak through.
guerrilla 4y ago
Why not frama-c instead?
- ryao 4y ago
  You could submit frama-c as a hacker news link. That said, frama-c suffers from a documentation problem. It has so much documentation that it either lacks good documentation explaining how to navigate its documentation, or it has that documentation and it is not easy to find. :/
  - rwmj 4y ago
    FWIW I explored frama-c a bit and made a video about it: http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 It's an internal Red Hat tech talk but I don't think anyone's going to mind.
emmanueloga_ 4y ago
Does anybody know how does this compare to https://compcert.org/ https://compcert.org/ ?
- ryao 4y ago
  It does not. One is a language extension that claims to prevent certain classes of issues. The other is a C compiler that claims to do nothing to prevent those classes of issues. The two are not comparable at all. You would be better off comparing it to Astree, which is a static analyzer written by the group that wrote the Compcert C compiler. https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm Astree claims to be able to prove the absence of use-after-free, which the checked C documentation says that checked C does not prevent. You would need to check to see if Astree can prove the absence of all of the issues that checked C is intended to prevent, but at a glance that seems possible. In theory, Astree can be used to fix all of them by doing fixes until it stops complaining.
  - ryao 4y ago
    > You would be better off comparing it to Astree, which is a static analyzer written by the group that wrote the Compcert C compiler. I was wrong to write this. They were written by different groups in France, but licenses for both of them are being sold by the same company, which made it easy to mistake the creators as the same group. I realized my misunderstanding several hours after making that comment and could not edit to correct the error.
ummonk 4y ago
Why does it need to be done as an extension? Can't you use fat pointers and crash the program if the bounds check fails? Since it's undefined behavior, this should be compatible with the C specification.
- rwmj 4y ago
  I'm a bit confused by what you're proposing, but I will say that the problem with fat pointers is they are incompatible with existing compiled libraries, meaning you usually need to recompile absolutely everything (including libc). There are only limited circumstances where this is acceptable (or possible).
NetOpWibby 4y ago
Typescript C?

264 points by soheilpro 4y ago

Quite honestly, I love what MS has done with JavsScript with Typescript. It would be great if they could do the same for C. I guess the hard part will be the fact that all your dependent libraries will (likely) still be unsafe.

pjmlp 4y ago
See also https://devblogs.microsoft.com/cppblog/high-confidence-lifetime-checks-in-visual-studio-version-17-5-preview-2/ https://devblogs.microsoft.com/cppblog/high-confidence-lifet...
- flohofwoe 4y ago
  I'm a bit confused, at the start they talk about C++, but some of the code examples look like C. Do those checks also work in the C compiler? (the difference is kinda important, because unlike Clang, the MSVC C++ compiler doesn't have enough non-standard language extensions to compile C code that was written in the last 20 years).
  - pjmlp 4y ago
    They talk about C++, because that is what mostly matters to Visual C++ customers, however /analyse mode also works in C code. https://learn.microsoft.com/en-us/cpp/code-quality/code-analysis-for-c-cpp-overview?view=msvc-170 https://learn.microsoft.com/en-us/cpp/code-quality/code-anal...
    - sendfoods 4y ago
      I'm a bit confused. Didn't Herb Sutter essentially fork clang and extended the codebase in the beginning? Is microsoft working with that fork and (most importantly) re-contributing?
      - pjmlp 4y ago
        If you mean cpp2, that has nothing to do with Microsoft, it's Herb's personal project.
        sendfoods 4y ago
        No, his lifetime work, e.g. https://herbsutter.com/2018/09/20/lifetime-profile-v1-0-posted/ https://herbsutter.com/2018/09/20/lifetime-profile-v1-0-post...
        pjmlp 4y ago
        No that was a proof of concept for a paper that went nowhere. VC++ analysis builds up on SAL infrastructure. https://learn.microsoft.com/en-us/cpp/code-quality/understanding-sal?view=msvc-170 https://learn.microsoft.com/en-us/cpp/code-quality/understan... "Closing the Gap between Rust and C++ Using Principles of Static Analysis - CppCon 2020" https://www.youtube.com/watch?v=_pQGRr4P16w https://www.youtube.com/watch?v=_pQGRr4P16w There is also a clang work on lifetimes, but little progress has happened since 2019. "Lifetime analysis for everyone - CppCon 2019" https://www.youtube.com/watch?v=d67kfSnhbpA https://www.youtube.com/watch?v=d67kfSnhbpA
        sendfoods 4y ago
        SAL, as I understand it, is Visual Studio/Microsoft only? Do you have any idea if this work will make it to clang/gcc/g++?
        int_19h 4y ago
        SAL is deliberately designed such that it can be defined as a bunch of macros that expand to whatever compiler-specific magic the implementation needs (e.g. MSYS64 doesn't support it at all, but they define all those macros as no-op, so code still compiles). So in principle it could work across implementations.
phailhaus 4y ago
I'm begging them to do the same for Python.
- corndoge 4y ago
  They made pyright which is pretty rad
  - phailhaus 4y ago
    Yeah it's pretty great, but still hamstrung by the inherent limitations of the language itself. Would love to see a new language on top of Python that treats types as first-class constructs.
    - still_grokking 4y ago
      Why "on top of Python"? The runtime is slow as hell, limited and actually very aged. But there are better modern alternatives. https://docs.scala-lang.org/scala3/book/scala-for-python-devs.html https://docs.scala-lang.org/scala3/book/scala-for-python-dev... Types in Scala are not only "first-class". You can even program with them like in TS. https://blog.rockthejvm.com/type-level-programming-scala-3/ https://blog.rockthejvm.com/type-level-programming-scala-3/ (Type level functions are correctness proves, BTW.) Enjoy!
      - still_grokking 4y ago
        I guess I should have mentioned that Scala 3, with its new syntax, look almost like "Python with types". That's why I've mentioned it.

pjmlp 4y ago

Older discussions on Checked C, https://news.ycombinator.com/item?id=30321535 https://news.ycombinator.com/item?id=30321535 https://news.ycombinator.com/item?id=19424106 https://news.ycombinator.com/item?id=19424106

belter 4y ago

"A Formal Model of Checked C" - https://news.ycombinator.com/item?id=30321535 https://news.ycombinator.com/item?id=30321535 - 37 comments - 10 months ago "Checked C" - https://news.ycombinator.com/item?id=26190403 https://news.ycombinator.com/item?id=26190403 - 133 comments - 2021 "Refactoring the FreeBSD Kernel with Checked C" - https://news.ycombinator.com/item?id=25989115 https://news.ycombinator.com/item?id=25989115 - 41 comments - 2021 "Achieving Safety Incrementally with Checked C" - https://news.ycombinator.com/item?id=19424106 https://news.ycombinator.com/item?id=19424106 - 21 comments - 2019 "Checked C: Making C Safer by Extension" - https://news.ycombinator.com/item?id=17939537 https://news.ycombinator.com/item?id=17939537 - 55 comments - 2018 "Checked C: extension to C that adds static and dynamic checking" - https://news.ycombinator.com/item?id=16588483 https://news.ycombinator.com/item?id=16588483 - 92 comments - 2018 "Checked C" - https://news.ycombinator.com/item?id=11899925 https://news.ycombinator.com/item?id=11899925 - 156 comments - 2016

dang 4y ago
Thanks! Added a few: C to Checked C by 3C - https://news.ycombinator.com/item?id=30857289 https://news.ycombinator.com/item?id=30857289 - March 2022 (1 comment) A Formal Model of Checked C - https://news.ycombinator.com/item?id=30321535 https://news.ycombinator.com/item?id=30321535 - Feb 2022 (37 comments) Why Checked C when there was Verona? - https://news.ycombinator.com/item?id=26499846 https://news.ycombinator.com/item?id=26499846 - March 2021 (2 comments) Checked C - https://news.ycombinator.com/item?id=26190403 https://news.ycombinator.com/item?id=26190403 - Feb 2021 (133 comments) Refactoring the FreeBSD Kernel with Checked C [pdf] - https://news.ycombinator.com/item?id=25989115 https://news.ycombinator.com/item?id=25989115 - Feb 2021 (41 comments) Refactoring the FreeBSD Kernel with Checked C [pdf] - https://news.ycombinator.com/item?id=24019185 https://news.ycombinator.com/item?id=24019185 - Aug 2020 (13 comments) Achieving Safety Incrementally with Checked C - https://news.ycombinator.com/item?id=19424106 https://news.ycombinator.com/item?id=19424106 - March 2019 (21 comments) Checked C: Making C Safer by Extension - https://news.ycombinator.com/item?id=17939537 https://news.ycombinator.com/item?id=17939537 - Sept 2018 (55 comments) Checked C: extension to C that adds static and dynamic checking - https://news.ycombinator.com/item?id=16588483 https://news.ycombinator.com/item?id=16588483 - March 2018 (92 comments) Checked C - https://news.ycombinator.com/item?id=12049548 https://news.ycombinator.com/item?id=12049548 - July 2016 (3 comments) Checked C – A Safer C/C++ from Microsoft - https://news.ycombinator.com/item?id=11936418 https://news.ycombinator.com/item?id=11936418 - June 2016 (3 comments) Checked C - https://news.ycombinator.com/item?id=11899925 https://news.ycombinator.com/item?id=11899925 - June 2016 (156 comments)

WalterBright 4y ago

Checked C: int a[5] = { 0, 1, 2, 3, 4}; _Array_ptr<int> p : count(5) = a; // p points to 5 elements. My proposal for C: int a[5] = { 0, 1, 2, 3, 4}; int p[..] = a; // p points to 5 elements. https://www.digitalmars.com/articles/C-biggest-mistake.html https://www.digitalmars.com/articles/C-biggest-mistake.html https://github.com/Microsoft/checkedc/wiki/New-pointer-and-array-types#checked-single-dimensional-arrays https://github.com/Microsoft/checkedc/wiki/New-pointer-and-a...

KingLancelot 4y ago
Fat pointers are a good idea, but I think it’d be a better idea to store the start and evd pointers instead of a pointer to the first element and a size_t.
- 1980phipsi 4y ago
  Why?
  - masklinn 4y ago
    I'd guess it's because that's what C++ does. Though it's unclear to me that C++-style iteration (where you increment a running pointer until you reach an EOI pointer) is much used in C.
    - WalterBright 4y ago
      Storing two pointers into the same array is a memory safety problem. It's hard to implement a borrow checker when there are two live mutable pointers into the same memory object.
      - int_19h 4y ago
        I would expect the borrow checker to treat a slice as a logical pointer to all elements that are addressable through it, regardless of how it's implemented under the hood.

jimbob45 4y ago

Why not just use C++? Also why can we not get better syntax for C? Function pointer syntax is so bad that people actively avoid using them. #pragma once is a hack. Every string library function is actively dangerous in addition to puts/gets. I know that nobody wants to be the one to mess with the core language and ruin it but this is awfully low-hanging fruit that hasn’t been fixed in 50 years.

mirekrusin 4y ago
It has been fixed. The fix has the codename "zig".
- shrimp_emoji 4y ago
  I heard it was "Rust".
  - chaosite 4y ago
    Rust is more comparable to C++ than C.
  - anfilt 4y ago
    Rust is not exactly a C replacement. Definitely the better choice these days over C++ in my opinion if you can use rust. It can be made to function more like C with #![no_std]. However that is an even less than batteries included experience than C.
    - masklinn 4y ago
      > Rust is not exactly a C replacement. Rust is absolutely a C replacement. Whether C heads want to use it is a more complicated question. But some are very much into it (e.g. Brian Cantrill). > It can be made to function more like C with #![no_std]. However that is an even less than batteries included experience than C. std assumes you have a heap and IO, which most C environments do. no_std removes all that (leaving only libcore as baseline), however you can re-add a dependency on "alloc" to get allocations and most of the standard collections back (all but hashset and hashmap, because no secure RNG). You can also / instead fill your needs with third-party crates more dedicated to restricted or freestanding environments, like heapless (https://crates.io/crates/heapless https://crates.io/crates/heapless).

gavinray 4y ago

Note that active development seems to be continuing here: https://github.com/secure-sw-dev/checkedc-llvm-project https://github.com/secure-sw-dev/checkedc-llvm-project

kelnos 4y ago

Thinking about this at a higher level, the real problem is that we use C arrays at all. But we can't stop using C arrays, because libc and a huge body of other C libraries out there represent lists of data using C arrays. As a useful counterexample, glib has GArray, GPtrArray, and GList, along with functions that you use to manipulate the lists. Those functions are presumably implemented correctly, and will prevent you from making out-of-bounds accesses. But of course those things are not widely adopted, because they're not standardized, they're not in libc, and libc has not been reimagined such that all of its APIs take and return these safer list primitives instead of bare C arrays. (And sure, GArray etc. are not necessarily suitable everywhere, as they require heap allocations. But I could imagine a safe abstraction that could allow for using stack or static allocations to back it.) So I see something like Checked C as a band-aid, when the language and stdlib just needs a complete overhaul. Obviously that's incredibly unlikely to ever happen, so something like Checked C is a decent compromise, I guess.

sramsay 4y ago
> As a useful counterexample, glib has GArray, GPtrArray, and GList, along with functions that you use to manipulate the lists. Those functions are presumably implemented correctly, and will prevent you from making out-of-bounds accesses. > But of course those things are not widely adopted, because they're not standardized, they're not in libc, and libc has not been reimagined such that all of its APIs take and return these safer list primitives instead of bare C arrays. I'm really not sure why the second thing is regarded by C programmers as such an insuperable barrier to the first thing. I absolutely understand that there are circumstances where extreme portability is a major requirement. That, and C's ability to operate in highly constrained environments are among its most laudable features. But many of us (including me) write user-facing C applications that have neither requirement and where Glib is either already installed or easy to install. Why not just go ahead and use it? If you're trying to get it to run on a tiny embedded system or in some land without Glib . . . well, this isn't the program for you! I feel like this is more of a weird cultural prejudice than a technical matter. People run programs in JavaScript (or Haskell, or Python) with hundreds of dependencies, and while some find that annoying, I don't hear people in these communities objecting to idea of dependencies the way people do with C. Could the standard library be better? Of course. But there's something to be said for not including a lot of batteries in the standard and just using the third-party tools that are available.

nottorp 4y ago

Hmm. Didn't Turbo Pascal have array bounds checking 3 billion years ago when we all had pet dinosaurs? It could have simply been added to the compiler in C as well...

baq 4y ago
Turbo Pascal had a lot of good ideas back in the late 80s and early 90s which were ridiculed back then and are now considered best practices… modules, safe strings, safe arrays, Delphi added quite nice objects. Alas, it was never popular in the Internet age. Just imagine if we had pascalscript instead of JavaScript - a decade of wasted developer time saved…
- tored 4y ago
  Correct me if I’m wrong but didn’t a few BASIC dialects, like QuickBasic and Turbo Basic, also support that back then? Truly bizarre that we ended up with C, still feature incomplete compared to what was available at the time.
  - 0xbadcafebee 4y ago
    The history of technology is littered with examples of a technically superior solution being abandoned for a crappier solution.
  - pjmlp 4y ago
    All major systems programming languages starting with JOVIAL in 1958, had bounds checking. ESPOL/NEWP from 1961, almost a decade before C came to be, even had unsafe code blocks!
- Tozen 4y ago
  There are those that would argue that the reasons for Pascal being lesser known than it should, involve the machinations of AT&T, other corporate entities, and orchestrated negative media. Pascal was in the way of what they were trying to push. And if people look deeper, there are some surprising elements of Pascal in newer languages, more than many realize. At some point, sanity and common sense will sneak through.

guerrilla 4y ago

Why not frama-c instead?

ryao 4y ago
You could submit frama-c as a hacker news link. That said, frama-c suffers from a documentation problem. It has so much documentation that it either lacks good documentation explaining how to navigate its documentation, or it has that documentation and it is not easy to find. :/
- rwmj 4y ago
  FWIW I explored frama-c a bit and made a video about it: http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 http://oirase.annexia.org/tmp/2020-frama-c-tech-talk.mp4 It's an internal Red Hat tech talk but I don't think anyone's going to mind.

emmanueloga_ 4y ago

Does anybody know how does this compare to https://compcert.org/ https://compcert.org/ ?

ryao 4y ago
It does not. One is a language extension that claims to prevent certain classes of issues. The other is a C compiler that claims to do nothing to prevent those classes of issues. The two are not comparable at all. You would be better off comparing it to Astree, which is a static analyzer written by the group that wrote the Compcert C compiler. https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm Astree claims to be able to prove the absence of use-after-free, which the checked C documentation says that checked C does not prevent. You would need to check to see if Astree can prove the absence of all of the issues that checked C is intended to prevent, but at a glance that seems possible. In theory, Astree can be used to fix all of them by doing fixes until it stops complaining.
- ryao 4y ago
  > You would be better off comparing it to Astree, which is a static analyzer written by the group that wrote the Compcert C compiler. I was wrong to write this. They were written by different groups in France, but licenses for both of them are being sold by the same company, which made it easy to mistake the creators as the same group. I realized my misunderstanding several hours after making that comment and could not edit to correct the error.

ummonk 4y ago

Why does it need to be done as an extension? Can't you use fat pointers and crash the program if the bounds check fails? Since it's undefined behavior, this should be compatible with the C specification.

rwmj 4y ago
I'm a bit confused by what you're proposing, but I will say that the problem with fat pointers is they are incompatible with existing compiled libraries, meaning you usually need to recompile absolutely everything (including libc). There are only limited circumstances where this is acceptable (or possible).

NetOpWibby 4y ago

Typescript C?