7 ms·

Related but more high level, I think we should have language sets instead of single languages with simpler interop and shared infra: https://gist.github.com/xix

Related but more high level, I think we should have language sets instead of single languages with simpler interop and shared infra: https://gist.github.com/xixixao/8e363dbd3663b6729cd5b6d74dbbf9d4 https://gist.github.com/xixixao/8e363dbd3663b6729cd5b6d74dbb...

simpleguitar 5y ago
I love this concept!
jeofken 5y ago
Love this
janpaul123 5y ago
Yes!!
woojoo666 5y ago
Cool idea! It seems like you are trying to extend the whole "optional types" idea of Typescript further to add optional low level programming. One thing that came to mind. One of the major reasons why Typescript's optional/gradual typing system works so well is because the the type system and the runtime logic are mostly orthogonal. All the types that are used and declared in typescript, are stripped away by the compiler and don't affect the javascript logic. This means that if I import some other team's typescript code, I can freely write javascript on top without worrying. Low-level operations like manual memory management are not like that. They are part of the runtime, and _do_ affect the business logic. It's a leaky abstraction. So if I import some other team's Rust code and I try to write RustScript on top, I might have to worry about some special edge cases where the argument I pass in isn't properly garbage collected or what not.
creativemonkeys 5y ago
As far as I can tell, D already implements this idea. The Rust/RustGC duality is very similar to D's approach, which has manual memory management and an optional GC [1], and DMDScript [2] could be the scripting language. [1] https://dlang.org/spec/garbage.html https://dlang.org/spec/garbage.html [2] https://github.com/DigitalMars/DMDScript https://github.com/DigitalMars/DMDScript
- mhh__ 5y ago
  D is the scripting language. The whole benefit of D for the company I work for is that we only have one language.
  - moonchild 5y ago
    Sil is distinct from d, and has distinct goals.
    - mhh__ 5y ago
      If we did SIL in C++ there's a good chance it'd have something like the UE4 header preprocessor to deal with all the hooks/metaprogramming we were able to D directly in D.
qpafqx 5y ago
Would you say Ruby, Elixir, and Crystal are an example of such language sets?
bnert 5y ago
Agreed, this is compelling!
jiggawatts 5y ago
I’ve had similar notions. For example, Rust used to have a garbage collector. A language set boundary would be a good way to add this back in without requiring a runtime at the lower levels. Rust already has “levels”, such as no-std or core. Similarly C# has a scripting variant: https://visualstudiomagazine.com/articles/2021/06/14/csharp-scripting.aspx?m=1 https://visualstudiomagazine.com/articles/2021/06/14/csharp-... And it also supports AoT compilation to a single EXE, but there were a lot of limitations. The latest attempt is a WIP: https://github.com/dotnet/runtime/issues/61231 https://github.com/dotnet/runtime/issues/61231 I would argue that libraries especially need highly restricted language subsets. E.g.: an image parser library should be “pure” in the sense of never being permitted to access system APIs. Image binary in, decoded bitmap out. Like a pure function, but at the module level.
- pjmlp 5y ago
  There are various approaches to native compilation on .NET. NGEN which was there since day one, but its main purpose was fast startup and only allows for dynamic linking. Mono AOT one, used by Xamarin workloads for iOS and Android deployments. The Sing# and System C# dialects used by Singularity and Midori respectively. The MDIL used by Windows Phone 8 and 8.1, based on Singularity's Bartok compiler. .NET Native introduced in Windows 10 for UWP workloads, replacing the MDIL based one, originally known as Project N. The NativeAOT pointed by you, which started as a research project on how to bring .NET Native back into main .NET. Finally some alternative ones like Unity's IL2CPP or CosmOS.
- zozbot234 5y ago
  Rust is getting support for local allocators/arenas as part of its core library. So it could become quite feasible to get support for tracing and garbage collection within a specific arena, with outside "GC roots" being managed by the borrow checker. You'd be fine as long as nothing in there tried to link back to your "GC roots". Similarly, "leaf" allocations could also live outside the GC arena provided that they did not try to link back into it. Either of these constraints seems like it could be checked during compile.
moonchild 5y ago
Common lisp can be and has been successfully used for high-performance numerics[0] as well as low-level system code[1], all while being a high-level, garbage-collected language. (The latter property likely leading to better overall performance in large programs.) Verification may be interesting, for high-assurance (e.g. automotive/aerospace) applications. It's for this reason that a theorem prover[2] and an ml[3] have been implemented, and they interoperate freely with the rest of common lisp. In other words: we are already where you want to be, and we are even less stratified than you propose we would need to be. 0. https://github.com/marcoheisig/Petalisp https://github.com/marcoheisig/Petalisp 1. https://github.com/froggey/mezzano/ https://github.com/froggey/mezzano/ 2. https://www.cs.utexas.edu/users/moore/acl2/ https://www.cs.utexas.edu/users/moore/acl2/ 3. https://github.com/coalton-lang/coalton https://github.com/coalton-lang/coalton
- mhh__ 5y ago
  Is there a example formally verified common lisp project to look at? Either pedagogical (I'm impressed by lisp but ultimately not particularly familiar with it) or impressive like CompCert is for Coq perhaps.
  - moonchild 5y ago
    I don't know; I haven't paid close attention to such things. But pulling on the acl2 thread will probably lead somewhere. Also maybe of interest, not quite the same but on vaguely parallel lines, minikanren and microkanren.
3np 5y ago
One already exists: Python+mypy+cython https://cython.readthedocs.io/en/latest/src/tutorial/memory_allocation.html https://cython.readthedocs.io/en/latest/src/tutorial/memory_...

simpleguitar 5y ago

I love this concept!

jeofken 5y ago

Love this

janpaul123 5y ago

Yes!!

woojoo666 5y ago

Cool idea! It seems like you are trying to extend the whole "optional types" idea of Typescript further to add optional low level programming. One thing that came to mind. One of the major reasons why Typescript's optional/gradual typing system works so well is because the the type system and the runtime logic are mostly orthogonal. All the types that are used and declared in typescript, are stripped away by the compiler and don't affect the javascript logic. This means that if I import some other team's typescript code, I can freely write javascript on top without worrying. Low-level operations like manual memory management are not like that. They are part of the runtime, and _do_ affect the business logic. It's a leaky abstraction. So if I import some other team's Rust code and I try to write RustScript on top, I might have to worry about some special edge cases where the argument I pass in isn't properly garbage collected or what not.

creativemonkeys 5y ago

As far as I can tell, D already implements this idea. The Rust/RustGC duality is very similar to D's approach, which has manual memory management and an optional GC [1], and DMDScript [2] could be the scripting language. [1] https://dlang.org/spec/garbage.html https://dlang.org/spec/garbage.html [2] https://github.com/DigitalMars/DMDScript https://github.com/DigitalMars/DMDScript

mhh__ 5y ago
D is the scripting language. The whole benefit of D for the company I work for is that we only have one language.
- moonchild 5y ago
  Sil is distinct from d, and has distinct goals.
  - mhh__ 5y ago
    If we did SIL in C++ there's a good chance it'd have something like the UE4 header preprocessor to deal with all the hooks/metaprogramming we were able to D directly in D.

qpafqx 5y ago

Would you say Ruby, Elixir, and Crystal are an example of such language sets?

bnert 5y ago

Agreed, this is compelling!

jiggawatts 5y ago

I’ve had similar notions. For example, Rust used to have a garbage collector. A language set boundary would be a good way to add this back in without requiring a runtime at the lower levels. Rust already has “levels”, such as no-std or core. Similarly C# has a scripting variant: https://visualstudiomagazine.com/articles/2021/06/14/csharp-scripting.aspx?m=1 https://visualstudiomagazine.com/articles/2021/06/14/csharp-... And it also supports AoT compilation to a single EXE, but there were a lot of limitations. The latest attempt is a WIP: https://github.com/dotnet/runtime/issues/61231 https://github.com/dotnet/runtime/issues/61231 I would argue that libraries especially need highly restricted language subsets. E.g.: an image parser library should be “pure” in the sense of never being permitted to access system APIs. Image binary in, decoded bitmap out. Like a pure function, but at the module level.

pjmlp 5y ago
There are various approaches to native compilation on .NET. NGEN which was there since day one, but its main purpose was fast startup and only allows for dynamic linking. Mono AOT one, used by Xamarin workloads for iOS and Android deployments. The Sing# and System C# dialects used by Singularity and Midori respectively. The MDIL used by Windows Phone 8 and 8.1, based on Singularity's Bartok compiler. .NET Native introduced in Windows 10 for UWP workloads, replacing the MDIL based one, originally known as Project N. The NativeAOT pointed by you, which started as a research project on how to bring .NET Native back into main .NET. Finally some alternative ones like Unity's IL2CPP or CosmOS.
zozbot234 5y ago
Rust is getting support for local allocators/arenas as part of its core library. So it could become quite feasible to get support for tracing and garbage collection within a specific arena, with outside "GC roots" being managed by the borrow checker. You'd be fine as long as nothing in there tried to link back to your "GC roots". Similarly, "leaf" allocations could also live outside the GC arena provided that they did not try to link back into it. Either of these constraints seems like it could be checked during compile.

moonchild 5y ago

Common lisp can be and has been successfully used for high-performance numerics[0] as well as low-level system code[1], all while being a high-level, garbage-collected language. (The latter property likely leading to better overall performance in large programs.) Verification may be interesting, for high-assurance (e.g. automotive/aerospace) applications. It's for this reason that a theorem prover[2] and an ml[3] have been implemented, and they interoperate freely with the rest of common lisp. In other words: we are already where you want to be, and we are even less stratified than you propose we would need to be. 0. https://github.com/marcoheisig/Petalisp https://github.com/marcoheisig/Petalisp 1. https://github.com/froggey/mezzano/ https://github.com/froggey/mezzano/ 2. https://www.cs.utexas.edu/users/moore/acl2/ https://www.cs.utexas.edu/users/moore/acl2/ 3. https://github.com/coalton-lang/coalton https://github.com/coalton-lang/coalton

mhh__ 5y ago
Is there a example formally verified common lisp project to look at? Either pedagogical (I'm impressed by lisp but ultimately not particularly familiar with it) or impressive like CompCert is for Coq perhaps.
- moonchild 5y ago
  I don't know; I haven't paid close attention to such things. But pulling on the acl2 thread will probably lead somewhere. Also maybe of interest, not quite the same but on vaguely parallel lines, minikanren and microkanren.

3np 5y ago

One already exists: Python+mypy+cython https://cython.readthedocs.io/en/latest/src/tutorial/memory_allocation.html https://cython.readthedocs.io/en/latest/src/tutorial/memory_...