6 ms·

Author here. Yeah, you shouldn't believe it yet, but here is the status of each: * "As powerful as C": unproven. I might need something like Rust's `unsafe`,

Author here. Yeah, you shouldn't believe it yet, but here is the status of each: * "As powerful as C": unproven. I might need something like Rust's `unsafe`, and even though I have something in mind for that, it requires that any program be expressible in Dynamic Restricted Structured Concurrency, an open problem. I am working on a proof, though. * "As flexible as Lisp": I think this is proven. Yao has equivalents for both macros (keywords) and reader macros (lexing modes). My build system uses its own keywords to implement a build DSL [1]. The shell sublanguage uses a lexing mode, and another makes it possible to embed JSON. * "As easy as Python": in retrospect, this isn't quite possible, but I hope to get 90% of the way. * "As provable as Ada/SPARK": I'll let you read the design in [2] and decide for yourself. But Yao will also have contracts. * "More reliable than Rust": unproven, but I think the lack of async will go a long way. * "With the time semantics of HAL/S": unproven. HAL/S was what the Shuttle software was written in [3]. It was hard real-time. Because Yao will be distributed in IR form [4], the back end could leverage knowledge of worst-case instruction latencies to calculate worst-case response times. This same thing will also allow using only constant-time instructions for cryptography, using a `constant_time` function trait. [1]: https://rigbuild.dev/build.rig5/#keywords https://rigbuild.dev/build.rig5/#keywords [2]: https://gavinhoward.com/2024/05/what-rust-got-wrong-on-formal-verification/ https://gavinhoward.com/2024/05/what-rust-got-wrong-on-forma... [3]: https://www.fastcompany.com/28121/they-write-right-stuff https://www.fastcompany.com/28121/they-write-right-stuff [4]: https://gavinhoward.com/2024/09/rewriting-rust-a-response/#distribution https://gavinhoward.com/2024/09/rewriting-rust-a-response/#d...

az09mugen 2y ago
Thank you very much for your detailed answer. Will look into your links right now.
az09mugen 2y ago
Hats off, you really did in fact a deep analysis of Rust conceptual errors by searching alternative ways to fix Rust async. Also by understanding and describing the decisions you made and what are their architectural implications (I liked the good, the bad and the ugly part). While I can't appreciate the entirety of this language because I can't grasp all the technical subtilities, I really like the core ideas at the basis of Yao and the spirit you put into it. I hope I can play with this language some day. And wish you good luck with this nice project.
- gavinhoward 2y ago
  This is one of the nicest, yet honest, compliments I have ever received. Thank you!
AlotOfReading 2y ago
Worst case execution times are generally unknowable, even at codegen. It depends on things like the specific microarchitectural details, what other instructions are currently executing, the memory hierarchy, what instructions have been executed before, how the power supply is responding, what the thermal environment is like, etc. HAL/S dealt with these problems by a combination of programmer/validation discipline, custom hardware designed for hard real-time usecases, and generous support from the underlying RTOS (FCOS). Cryptography code doesn't deal with it, it just avoids data dependent nondeterminism, which is good enough for those use cases.
- gavinhoward 2y ago
  Yes, you are correct. My idea is to cause a compile error if the backend can't use all instructions for which it knows the worst case latency or if it can't use purely constant-time instructions.
  - AlotOfReading 2y ago
    That's essentially every instruction though. You can't write a program that doesn't access memory for example, and every memory access is nondeterministic in wall clock time.
    - gavinhoward 2y ago
      Yes. In the crypto example, the backend would have to be sophisticated enough to know when the same addresses would be accessed every time, like bitslicing in AES. [1] The devil absolutely is in the details. This is why I say Yao's capabilities on this front are unproven. [1]: https://www.bearssl.org/constanttime.html#constant-time-in-bearssl https://www.bearssl.org/constanttime.html#constant-time-in-b...
xedrac 2y ago
> As flexible as Lisp": I think this is proven. Given the development model of Lisp is modifying a live image of a running program, I have to assume you limited this statement to the availability of macros.
- gavinhoward 2y ago
  Yes, sorry. I should clarify that.
- lispm 2y ago
  > Given the development model of Lisp is modifying a live image of a running program I would say it is modifying the running program itself. An image is the saved version of the heap. Saving/loading images is optional. But with Lisp one can also compile source files to compiled files. In rare occasions it is also possible to compile whole programs.
xavxav 2y ago
> * "As provable as Ada/SPARK": I'll let you read the design in [2] and decide for yourself. But Yao will also have contracts. Without being too self-indulgent, I'm not sure there is that big of a gap between the two in provability, there are now a huge array of verifiers for Rust code which are being used to verify real code: SAT/SMT solvers, kernels, memory allocators etc...
- gavinhoward 2y ago
  I agree. I think getting provability right would bring reliability along with it.
BoingBoomTschak 2y ago
> "As flexible as Lisp": I think this is proven. Yao has equivalents for both macros (keywords) and reader macros (lexing modes). First-class symbols (incl. uninterned symbols)? Classes and functions can be redefined at runtime? User-available parsing (read) and runtime compilation (compile)? Restarts? CLOS and MOP? Communication with the compiler (declarations and ClTl2 *-information)? I don't mean to sound too abrasive, but reducing Lisp flexibility to macros is a bit much. In any case, good luck with your project!
- gavinhoward 2y ago
  > First-class symbols (incl. uninterned symbols)? Yes. > Classes and functions can be redefined at runtime? No. > User-available parsing (read) and runtime compilation (compile)? Yes, though runtime compilation is not implemented yet. > Restarts? Yes, though they are only implemented in the runtime; the keywords don't exist yet. > CLOS and MOP? No, the object system will be more recognizable to non-Lispers. > Communication with the compiler (declarations and ClTl2 *-information)? I wasn't able to find info on these. I will keep looking, and I would appreciate pointers, but the answer is probably no. Edit: after skimming [1], the answer on declarations is probably yes, for the most part. Still searching for *-information stuff. Edit 2: After skimming [2], Yao originally didn't have any concept of stuff like the *-information functions, but those are good ideas, and I will add them. [1]: https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node105.html https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node105.html [2]: https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node102.html https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node102.html
  - BoingBoomTschak 2y ago
    Huh, thanks for replying seriously to my snark, that's more than what I expected! About CLOS, I suggest at least making method combination more flexible than C++'s override. A way to run both the parent and child methods is often needed (maybe in a specific order, maybe with a way to collect all the return values). Declarations are basically C/C++'s pragmas and __attribute__, but standardized and using a seamless syntax. The ClTl2 additions I'm talking about are ways for the compiler to give lexical information to macros: see https://github.com/Zulu-Inuoe/trivial-cltl2 https://github.com/Zulu-Inuoe/trivial-cltl2 and https://github.com/alex-gutev/cl-environments https://github.com/alex-gutev/cl-environments

az09mugen 2y ago

Thank you very much for your detailed answer. Will look into your links right now.

az09mugen 2y ago

Hats off, you really did in fact a deep analysis of Rust conceptual errors by searching alternative ways to fix Rust async. Also by understanding and describing the decisions you made and what are their architectural implications (I liked the good, the bad and the ugly part). While I can't appreciate the entirety of this language because I can't grasp all the technical subtilities, I really like the core ideas at the basis of Yao and the spirit you put into it. I hope I can play with this language some day. And wish you good luck with this nice project.

gavinhoward 2y ago
This is one of the nicest, yet honest, compliments I have ever received. Thank you!

AlotOfReading 2y ago

Worst case execution times are generally unknowable, even at codegen. It depends on things like the specific microarchitectural details, what other instructions are currently executing, the memory hierarchy, what instructions have been executed before, how the power supply is responding, what the thermal environment is like, etc. HAL/S dealt with these problems by a combination of programmer/validation discipline, custom hardware designed for hard real-time usecases, and generous support from the underlying RTOS (FCOS). Cryptography code doesn't deal with it, it just avoids data dependent nondeterminism, which is good enough for those use cases.

gavinhoward 2y ago
Yes, you are correct. My idea is to cause a compile error if the backend can't use all instructions for which it knows the worst case latency or if it can't use purely constant-time instructions.
- AlotOfReading 2y ago
  That's essentially every instruction though. You can't write a program that doesn't access memory for example, and every memory access is nondeterministic in wall clock time.
  - gavinhoward 2y ago
    Yes. In the crypto example, the backend would have to be sophisticated enough to know when the same addresses would be accessed every time, like bitslicing in AES. [1] The devil absolutely is in the details. This is why I say Yao's capabilities on this front are unproven. [1]: https://www.bearssl.org/constanttime.html#constant-time-in-bearssl https://www.bearssl.org/constanttime.html#constant-time-in-b...

xedrac 2y ago

> As flexible as Lisp": I think this is proven. Given the development model of Lisp is modifying a live image of a running program, I have to assume you limited this statement to the availability of macros.

gavinhoward 2y ago
Yes, sorry. I should clarify that.
lispm 2y ago
> Given the development model of Lisp is modifying a live image of a running program I would say it is modifying the running program itself. An image is the saved version of the heap. Saving/loading images is optional. But with Lisp one can also compile source files to compiled files. In rare occasions it is also possible to compile whole programs.

xavxav 2y ago

> * "As provable as Ada/SPARK": I'll let you read the design in [2] and decide for yourself. But Yao will also have contracts. Without being too self-indulgent, I'm not sure there is that big of a gap between the two in provability, there are now a huge array of verifiers for Rust code which are being used to verify real code: SAT/SMT solvers, kernels, memory allocators etc...

gavinhoward 2y ago
I agree. I think getting provability right would bring reliability along with it.

BoingBoomTschak 2y ago

> "As flexible as Lisp": I think this is proven. Yao has equivalents for both macros (keywords) and reader macros (lexing modes). First-class symbols (incl. uninterned symbols)? Classes and functions can be redefined at runtime? User-available parsing (read) and runtime compilation (compile)? Restarts? CLOS and MOP? Communication with the compiler (declarations and ClTl2 *-information)? I don't mean to sound too abrasive, but reducing Lisp flexibility to macros is a bit much. In any case, good luck with your project!

gavinhoward 2y ago
> First-class symbols (incl. uninterned symbols)? Yes. > Classes and functions can be redefined at runtime? No. > User-available parsing (read) and runtime compilation (compile)? Yes, though runtime compilation is not implemented yet. > Restarts? Yes, though they are only implemented in the runtime; the keywords don't exist yet. > CLOS and MOP? No, the object system will be more recognizable to non-Lispers. > Communication with the compiler (declarations and ClTl2 *-information)? I wasn't able to find info on these. I will keep looking, and I would appreciate pointers, but the answer is probably no. Edit: after skimming [1], the answer on declarations is probably yes, for the most part. Still searching for *-information stuff. Edit 2: After skimming [2], Yao originally didn't have any concept of stuff like the *-information functions, but those are good ideas, and I will add them. [1]: https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node105.html https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node105.html [2]: https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node102.html https://www.cs.cmu.edu/Groups/AI/html/cltl/clm/node102.html
- BoingBoomTschak 2y ago
  Huh, thanks for replying seriously to my snark, that's more than what I expected! About CLOS, I suggest at least making method combination more flexible than C++'s override. A way to run both the parent and child methods is often needed (maybe in a specific order, maybe with a way to collect all the return values). Declarations are basically C/C++'s pragmas and __attribute__, but standardized and using a seamless syntax. The ClTl2 additions I'm talking about are ways for the compiler to give lexical information to macros: see https://github.com/Zulu-Inuoe/trivial-cltl2 https://github.com/Zulu-Inuoe/trivial-cltl2 and https://github.com/alex-gutev/cl-environments https://github.com/alex-gutev/cl-environments