6 ms·

It's impossible to add a borrow checker to any existing language. The reason Rust has a working borrow checker is because every part of the language from struc

It's impossible to add a borrow checker to any existing language. The reason Rust has a working borrow checker is because every part of the language from structs, enum, traits, generics and all the way to the syntax itself has been designed to support lifetimes and borrow checking. It's is not something you can just tack on to an existing language without fundamentally changing it.

solatic 2mo ago
I wouldn't say it's impossible, rather un-ergonomic. TypeScript can add type information to ordinary JavaScript code via JSDoc comments; the result can both be executed as ordinary JavaScript as-is and type-checked with TypeScript. But it's a huge pain to try to write (and maintain) everything that way, it was supported as a hack to help migrate legacy codebases. You could probably take a similar "the lifetimes are embedded in comments" approach with other languages, and the result would be similarly un-ergonomic.
- afdbcreid 2mo ago
  That is possible (clang has experimental lifetime annotations support), but that is not enough to guarantee memory safety. As a simple example, Zig has no private fields. That makes encapsulating any unsafety impossible.
  - veber-alex 2mo ago
    Exactly. Every part of the language must support memory safety from first principles.
    - dnautics 2mo ago
      empirically untrue. several projects exist that bolt on extra safety to unsafe languages or unsafe parts of language. SeL4 for C, MIRI for rust unsafe. i guess ada/spark for ada too, is the OG, spark being added to ada 4 years after its first release
      - afdbcreid 2mo ago
        Hardening is definitely possible, we've had sanitizers in C/C++ for a long time. It's not full memory safety though. Miri is the same. SeL4C is formal verification, and while it can prove memory safety (and much more) it is much more difficult, to the point that you're basically programming in a different language. Ada/SPARK is your best example, and also the example I know the least of, so I won't comment on.
        kibwen 2mo ago
        SPARK omits some features of Ada, so it would only reinforce the sentiment that bolting on verifiability after-the-fact is difficult. Expressivity is generally the antithesis of static analysis, and it's very easy and tempting to make a language that is accidentally too expressive to support a given analysis without being required to make breaking changes to reduce expressivity.
        dnautics 2mo ago
        i mean in zig-clr it pushes you towards more expressive patterns, for example, making you label pointers as optional if their status is ambiguous
        kibwen 2mo ago
        A language is more expressive when it allows more programs and less expressive when it allows fewer programs. I don't know zig-clr, but if it rejects programs that Zig accepts (for example, by rejecting the aforementioned ambiguous pointers), then it is less expressive, not more (keeping in mind that being less expressive is not a pejorative).
        dnautics 2mo ago
        no thats not the definition of more expressive. more expressive means the language can encode more programmer intent without making a dog's breakfast of the code.
  - dnautics 2mo ago
    no. You don't need private fields. All you have to do is analyze the code, harness the compiler to generate a time-dependent data dependency graph, and map allocation/frees/uses, if you can 'color' branches where data are shared you can also track and check to see there isn't an aliasing violation too. it is easy to patch the zig compiler to enable this this (export the code graph; about 50 LOC). The analysis is much much harder to get right.
    - AlotOfReading 2mo ago
      It seems like it'd be pretty reasonable to get something akin to polonius. I can write up an engine in zig if it'd help?
      - dnautics 2mo ago
        start by examining zig-clr
    - rcxdude 2mo ago
      It is only feasible to do this if the whole of the codebase idea designed to allow it, and it's still going to blow up in odd ways of you don't have a way to describe lifetimes in your interfaces. The magic of rust's design is that it turns this memory tracking into a local problem, such that you can design an interface and be sure that every use case is safe and verifiably so.
    - afdbcreid 2mo ago
      This analysis is undecidable. There is a reason sound static analyzers (including languages like Rust) require in-code annotations.
      - dnautics 2mo ago
        it is possible to do in-code annotations in zig, if you're clever. you can get pretty far without them too. as an example, you can check for double free without ownership tagging, by being agnostic about who should free, and flagging if two nondisjoint code paths attempt to free the same allocation.
  - solatic 2mo ago
    > Zig has no private fields You may have missed the point here. You could add a comment to the struct field that marks the field as private, and build a TypeScript/JSDoc analogue that analyzes all accesses to the field and fails if it finds accesses from functions that aren't part of the struct that owns the field. You don't even need a comment on the field - you could copy Go's convention, add a comment to the struct definition marking it as "follows Go convention", and then fail any access from outside the struct to a field that starts with a lower-case character. It doesn't prevent you from ignoring that tool and writing Zig code that imports the struct and accesses the field. It is, of course, not part of the Zig language itself. But if you adopted a tool like that, it would be your responsibility to run it across-the-board and pay attention to the results - same as how it is your responsibility to pay attention to the results if you added those JSDoc comments.
    - afdbcreid 2mo ago
      I have picked private fields as an example of feature that is needed because it is very simple. You're right that you can build an analyzer (with additional code annotations) to support that, but it's only one example. Take another example: unsafe traits. They are fundamental to some safety encapsulations, most famously concurrency (`Send`/`Sync`). Here you cannot just build an analyzer to mark something unsafe, because Zig has no traits, its generics are duck-typed. You can, of course, add traits. But at this point you're essentially creating your own language that compiles to Zig, with all problems this entails (e.g. bad ecosystem support). It's also hard to claim that Zig can be memory safe then.
      - solatic 2mo ago
        > You can, of course, add traits. But at this point you're essentially creating your own language that compiles to Zig I think herein lies the rub. What's the difference between a static analysis tool and an actual separate language that transpiles to the original? Hypothetically - again, very un-ergonomically - you could add traits to Zig code in comments, or in example-traits.typezig files that would be skipped by the Zig compiler (like how *.d.ts files are skipped). How much of a language is writing code in a particular syntax, versus how much of a language is writing code that will pass a tool "building" it, versus how much of a language is about the final compiled output that you get from the tool? All static analysis tools that support line-level exceptions are, essentially, programmed by comments, with their own language (typically highly simplified compared to a "full" programming language), that affect whether or not the "language" passes or not. What Typescript/JSDoc shows is that, actually, much more complicated tooling can be built with this programming-by-comments model than had been done before (to my knowledge), and thus even more powerful still tooling could be built with that model. Of course there's a difference between static analysis and a language that transpiles. But perhaps it's more a question of degree than a simple binary classification.
- AlienRobot 2mo ago
  A better comparison would be Python. The way Python added types is the most disgusting thing imaginable... but it has type hints now, so I guess that makes some people happy.
dnautics 2mo ago
> It's impossible to add a borrow checker to any existing language. Why do you say that. Have you tried and failed? It seems to be possible to add a borrow checker to zig, just as you can add MIRI to rust to get extra safety in unsafe blocks.
pjmlp 2mo ago
Swift, Linear Haskell, Chapel, Ada/SPARK are all counter examples from such claim.
- lioeters 2mo ago
  Also OxCaml, from what I hear.
  - pjmlp 2mo ago
    Yes, it is getting there, however I would rather count it when they finally manage to upstream everything to OCaml as per plan.
  - rienbdj 2mo ago
    OCaml already starts form a memory safe base being GCd?
    - lioeters 2mo ago
      I'm not familiar but I think this paper describes how OxCaml works: Oxidizing OCaml with Modal Memory Management - https://dl.acm.org/doi/10.1145/3674642 https://dl.acm.org/doi/10.1145/3674642 > We focus on three mode axes: affinity, uniqueness and locality. Modes are fully backwards compatible with existing OCaml code and can be completely inferred. Our work makes manual memory management in OCaml safe and convenient and charts a path towards bringing the benefits of Rust to OCaml. https://github.com/oxcaml/oxcaml https://github.com/oxcaml/oxcaml
kfuse 2mo ago
C# was already a very mature language when it had referenes and later "ref safety" added to it.

solatic 2mo ago

I wouldn't say it's impossible, rather un-ergonomic. TypeScript can add type information to ordinary JavaScript code via JSDoc comments; the result can both be executed as ordinary JavaScript as-is and type-checked with TypeScript. But it's a huge pain to try to write (and maintain) everything that way, it was supported as a hack to help migrate legacy codebases. You could probably take a similar "the lifetimes are embedded in comments" approach with other languages, and the result would be similarly un-ergonomic.

afdbcreid 2mo ago
That is possible (clang has experimental lifetime annotations support), but that is not enough to guarantee memory safety. As a simple example, Zig has no private fields. That makes encapsulating any unsafety impossible.
- veber-alex 2mo ago
  Exactly. Every part of the language must support memory safety from first principles.
  - dnautics 2mo ago
    empirically untrue. several projects exist that bolt on extra safety to unsafe languages or unsafe parts of language. SeL4 for C, MIRI for rust unsafe. i guess ada/spark for ada too, is the OG, spark being added to ada 4 years after its first release
    - afdbcreid 2mo ago
      Hardening is definitely possible, we've had sanitizers in C/C++ for a long time. It's not full memory safety though. Miri is the same. SeL4C is formal verification, and while it can prove memory safety (and much more) it is much more difficult, to the point that you're basically programming in a different language. Ada/SPARK is your best example, and also the example I know the least of, so I won't comment on.
      - kibwen 2mo ago
        SPARK omits some features of Ada, so it would only reinforce the sentiment that bolting on verifiability after-the-fact is difficult. Expressivity is generally the antithesis of static analysis, and it's very easy and tempting to make a language that is accidentally too expressive to support a given analysis without being required to make breaking changes to reduce expressivity.
        dnautics 2mo ago
        i mean in zig-clr it pushes you towards more expressive patterns, for example, making you label pointers as optional if their status is ambiguous
        kibwen 2mo ago
        A language is more expressive when it allows more programs and less expressive when it allows fewer programs. I don't know zig-clr, but if it rejects programs that Zig accepts (for example, by rejecting the aforementioned ambiguous pointers), then it is less expressive, not more (keeping in mind that being less expressive is not a pejorative).
        dnautics 2mo ago
        no thats not the definition of more expressive. more expressive means the language can encode more programmer intent without making a dog's breakfast of the code.
- dnautics 2mo ago
  no. You don't need private fields. All you have to do is analyze the code, harness the compiler to generate a time-dependent data dependency graph, and map allocation/frees/uses, if you can 'color' branches where data are shared you can also track and check to see there isn't an aliasing violation too. it is easy to patch the zig compiler to enable this this (export the code graph; about 50 LOC). The analysis is much much harder to get right.
  - AlotOfReading 2mo ago
    It seems like it'd be pretty reasonable to get something akin to polonius. I can write up an engine in zig if it'd help?
    - dnautics 2mo ago
      start by examining zig-clr
  - rcxdude 2mo ago
    It is only feasible to do this if the whole of the codebase idea designed to allow it, and it's still going to blow up in odd ways of you don't have a way to describe lifetimes in your interfaces. The magic of rust's design is that it turns this memory tracking into a local problem, such that you can design an interface and be sure that every use case is safe and verifiably so.
  - afdbcreid 2mo ago
    This analysis is undecidable. There is a reason sound static analyzers (including languages like Rust) require in-code annotations.
    - dnautics 2mo ago
      it is possible to do in-code annotations in zig, if you're clever. you can get pretty far without them too. as an example, you can check for double free without ownership tagging, by being agnostic about who should free, and flagging if two nondisjoint code paths attempt to free the same allocation.
- solatic 2mo ago
  > Zig has no private fields You may have missed the point here. You could add a comment to the struct field that marks the field as private, and build a TypeScript/JSDoc analogue that analyzes all accesses to the field and fails if it finds accesses from functions that aren't part of the struct that owns the field. You don't even need a comment on the field - you could copy Go's convention, add a comment to the struct definition marking it as "follows Go convention", and then fail any access from outside the struct to a field that starts with a lower-case character. It doesn't prevent you from ignoring that tool and writing Zig code that imports the struct and accesses the field. It is, of course, not part of the Zig language itself. But if you adopted a tool like that, it would be your responsibility to run it across-the-board and pay attention to the results - same as how it is your responsibility to pay attention to the results if you added those JSDoc comments.
  - afdbcreid 2mo ago
    I have picked private fields as an example of feature that is needed because it is very simple. You're right that you can build an analyzer (with additional code annotations) to support that, but it's only one example. Take another example: unsafe traits. They are fundamental to some safety encapsulations, most famously concurrency (`Send`/`Sync`). Here you cannot just build an analyzer to mark something unsafe, because Zig has no traits, its generics are duck-typed. You can, of course, add traits. But at this point you're essentially creating your own language that compiles to Zig, with all problems this entails (e.g. bad ecosystem support). It's also hard to claim that Zig can be memory safe then.
    - solatic 2mo ago
      > You can, of course, add traits. But at this point you're essentially creating your own language that compiles to Zig I think herein lies the rub. What's the difference between a static analysis tool and an actual separate language that transpiles to the original? Hypothetically - again, very un-ergonomically - you could add traits to Zig code in comments, or in example-traits.typezig files that would be skipped by the Zig compiler (like how *.d.ts files are skipped). How much of a language is writing code in a particular syntax, versus how much of a language is writing code that will pass a tool "building" it, versus how much of a language is about the final compiled output that you get from the tool? All static analysis tools that support line-level exceptions are, essentially, programmed by comments, with their own language (typically highly simplified compared to a "full" programming language), that affect whether or not the "language" passes or not. What Typescript/JSDoc shows is that, actually, much more complicated tooling can be built with this programming-by-comments model than had been done before (to my knowledge), and thus even more powerful still tooling could be built with that model. Of course there's a difference between static analysis and a language that transpiles. But perhaps it's more a question of degree than a simple binary classification.
AlienRobot 2mo ago
A better comparison would be Python. The way Python added types is the most disgusting thing imaginable... but it has type hints now, so I guess that makes some people happy.

dnautics 2mo ago

> It's impossible to add a borrow checker to any existing language. Why do you say that. Have you tried and failed? It seems to be possible to add a borrow checker to zig, just as you can add MIRI to rust to get extra safety in unsafe blocks.

pjmlp 2mo ago

Swift, Linear Haskell, Chapel, Ada/SPARK are all counter examples from such claim.

lioeters 2mo ago
Also OxCaml, from what I hear.
- pjmlp 2mo ago
  Yes, it is getting there, however I would rather count it when they finally manage to upstream everything to OCaml as per plan.
- rienbdj 2mo ago
  OCaml already starts form a memory safe base being GCd?
  - lioeters 2mo ago
    I'm not familiar but I think this paper describes how OxCaml works: Oxidizing OCaml with Modal Memory Management - https://dl.acm.org/doi/10.1145/3674642 https://dl.acm.org/doi/10.1145/3674642 > We focus on three mode axes: affinity, uniqueness and locality. Modes are fully backwards compatible with existing OCaml code and can be completely inferred. Our work makes manual memory management in OCaml safe and convenient and charts a path towards bringing the benefits of Rust to OCaml. https://github.com/oxcaml/oxcaml https://github.com/oxcaml/oxcaml

kfuse 2mo ago

C# was already a very mature language when it had referenes and later "ref safety" added to it.