This property of dependent types:
> In fact, if you don't mind writing a proof or two, our sprintf function can be called on format strings that aren't fully known at compile-time! You only need to be able to prove that the string will have certain format specifiers, and then calling sprintf can typecheck.
It's not new to me, but I also find it pretty cool. Proving things at compile-time that certain runtime conditions will hold using a programming language is so much cooler than just proving it to yourself in your head or on paper, and then doing a runtime assertion in the actual code. Or, not doing a check at all, and just having crashes or security vulnerabilities if you're mistaken.
https://en.m.wikipedia.org/wiki/Curry%E2%80%93Howard_corresp...
It's actually not a lot of work and very rewarding to write a proof-checker that uses this principle.
This would allow simplifying the second stage massively because it is generated code and won't need ergonomy. This programming language would parse the sprintf format string exactly as if the compiled program would do it at runtime. When I read the article I thought to myself, aha, dependent types, could it be that it is similar to a user-provided program that computes the types?
I have to disclaim that designing programming languages is not my expertise. I am only an amateur.
These two stages avoid the complexity of Rust compile-time handling. Instead of hard coding things like lifetimes, generics, const generics, return position impl trait in trait (RPITIT), async fn in trait (AFIT), and so on, have a first stage standard library handling all these things.
And the third stage? A sandboxed interpreter with the same or similar syntax as the rest of the thing. I think this would be useful as glue code or just for tiny throw-away scripts. All these three stages would profit from a common base, so they should be provided together.
Makes sense?
The closest C function to this one is asprintf, because this function gives you back a new, separate string, which you may or may not decide to print. Just imagine if asprintf simply returned a char* pointing to an allocation by malloc, instead of taking an extra char ** as an out parameter.
char *my_sprintf(const char *, ...); void my_sprintf(char* format, ???) {
sprintf(format, ???);
}I know it's supposed to be pseudo code and most likely it's something like sprintf "% world %d" "hello" 42 but I got a little confused by the type list being backwards from what I expected
This paragraph shows that with a format string with an int format specifer, and then a string format specifier, the token list shows is exactly that, and the type it returns is a function that takes an Int and a String as input and returns a new string.
> For example, if the format string was "%d %s", the tokenization would be [IntFormat, NormalChar ' ', StrFormat], so the resulting type would be Int -> String -> String`. This might be confusing because it's a post-order traversal of the list, and might feel kind of backwards.
Isn't that exactly the order you'd expect?
I'm confused why it's called backwards, and why they say "post-order" traversal of a list, since I'm only used to hearing about traversing trees that way.
Isn't Int -> String -> String a shorthand for Int -> (String -> String)?
Thus I would have assumed the first argument to the result of sprintf "%s %d" would be an integer, then a string and the final result would be a string.
But the invocation would be sprintf "%s %d" "hello" 42, wouldn't it?