anqurvanillapy

9 ms·

1.
by anqurvanillapy 2y ago
Cool, and the paper mentioned in the document "Dependent Types for Low-Level Programming" [1] is such a gem. [1]: https://people.eecs.berkeley.edu/~necula/Papers/deputy-esop0...
2.
by anqurvanillapy 2y ago
I love your gradual approach pretty much. It sounds like gradual typing but not just the typing part. I used to make many tools with libclang Python bindings to automate some chores of refactoring. I don't remember if one could expand
3.
by anqurvanillapy 2y ago
> Build embedded or core OS code with it. things that do MMIO, DMA interactions, low level IO in kernel code or firmware (more embedded). I have a friend currently writing a GC in C and I was making it a project to test around my ideas (
4.
by anqurvanillapy 2y ago
> Offer real and significant benefits. Yeah! The criterion is just there like you said. > Do you have an opinion on the dotnet version of generics? I'm not familiar with dotnet languages, but I have much experience implementing g
5.
by anqurvanillapy 2y ago
> On the other hand I think we are in a local maxima with programming languages and type systems. I think I gotcha. Oh no. > But I haven't finished fleshing it out and proving the type system, so I really can't share it yet.
6.
by anqurvanillapy 2y ago
Love all the ideas here. I found it might be possible to tackle "strict aliasing" and "pointer provenance" with a type system and I would head down to it early. The approach might sound like Rust's `MaybeUninit` but
7.
by anqurvanillapy 2y ago
> But the only thing that really took off was effort to change things at the very base level rather than patch issues. Exactly, that's the most important takeaway I got from all the discussions here: I will be patching issues while
8.
by anqurvanillapy 2y ago
Notable approaches to compatibility with C might be: 1) LLVM, like Rust and Zig did (Zig stopped using it in 2023), since LLVM IR is good for being compatible and optimizing. 2) Other backends like libgccjit, I mentioned this because rustc
9.
by anqurvanillapy 2y ago
I love this idea so much. I got stuck at how to tackle "new language doesn't compile with a standard C compiler" for many times, but my solution is much worse than yours: Like LuaJIT, they left one unreadable "minilua&qu
10.
by anqurvanillapy 2y ago
Oh I heard about it and oops just hate myself for forgetting it. And the first sentence [1] of its pointer type introduction, exactly says everything I said here... > [...] greatest motivation behind ATS is to make it employed to constru
11.
by anqurvanillapy 2y ago
Woah I enjoyed the read a lot. I also learned that in LLVM IR, they have the implicit null checks [1] to replace the guard with just a signal handler, so it won't hurt the branch predictor too much. So I believe there are many options
12.
by anqurvanillapy 2y ago
Thanks for the mention! I heard about Carbon years ago but I'm happy this time I could dig it further for insights now. It's pretty fun to think about "Carbon to C++ is Kotlin to Java". One very important takeaway from a
13.
by anqurvanillapy 2y ago
That's true! Sorry that I didn't much clarify the "pain" though: It's quite like the experience of using parser combinator in Rust, where you could happily define the grammar and the parsing action using its existin
14.
by anqurvanillapy 2y ago
Thanks sooo much! I would definitely do it!
15.
by anqurvanillapy 2y ago
> Imagine writing large games in your language. You don’t. Read the features I listed. One ends up with a C alternative frontend (Cfront, if you love bad jokes) including type system like Zig without any standard library. No hash tables,
16.
by anqurvanillapy 2y ago
Exactly the kind of thoughts and insights I need from more of the users. Thank you for pointing out many concerns. > Headers. C++20 modules are left unstable and unused in major compilers there, but it’s a standard. And C is ironically p
17.
by anqurvanillapy 2y ago
> There are approaches e.g. Zig. Yes! Zig has done a great job on many C-related stuff, e.g. they've already made it possible to cross-compile C/C++ projects with Zig toolchain years ago. But I'm still quite stupidly obses
18.
by anqurvanillapy 2y ago
And then? https://github.com/anqurvanillapy/TinyLean
19.
by anqurvanillapy 2y ago
Ah that should be good for source-level compatibility. But I'm thinking about extending existing codebase that crosses between the kernel and user space, e.g. DPDK, SPDK, FUSE, kernel module, etc. Curious that how C3 would be adopted i
20.
by anqurvanillapy 2y ago
> We seem to have the same desire for a “cleaned up C.” That's so great! But sad that no enough ideas and argument came up here. :'( > How metaprogramming would work? When it comes to "tactics" in Coq and Lean 4 (i
21.
Ask HN: A retrofitted C dialect?
55 points by anqurvanillapy 2y ago|78 comments
22.
The Type Theory Podcast (2016)(typetheorypodcast.com)
1 points by anqurvanillapy 7y ago|0 comments
23.
The True Implementation of Pattern Matching in Python(github.com)
1 points by anqurvanillapy 7y ago|0 comments
24.
by anqurvanillapy 7y ago
No, this very paragraph is even highlighted in many major social media in China. The public opinions are oriented that people should be wise about products of Huawei.
25.
Graduate Texts in Mathematics(en.wikipedia.org)
4 points by anqurvanillapy 7y ago|0 comments
26.
Minitt-Rs: Extended Implementation of Mini-TT in Rust(github.com)
1 points by anqurvanillapy 7y ago|0 comments
27.
Session Types Revisited (2012) [pdf](dcs.gla.ac.uk)
2 points by anqurvanillapy 8y ago|0 comments
28.
Algebraic Presentations of Dependent Type Theories (2017)(arxiv.org)
3 points by anqurvanillapy 8y ago|0 comments
29.
Design and Implementation of the Andromeda Proof Assistant(arxiv.org)
1 points by anqurvanillapy 8y ago|0 comments
30.
LOOP (programming language)(en.wikipedia.org)
36 points by anqurvanillapy 8y ago|7 comments

More ›