artagnon

8 ms·

31.
by artagnon 4y ago
The example described in this post is JSON parsing in Haskell, but I've implemented a complicated compiler transform that lifts loops to static control parts (SCOPs), in the past, in C++. Each inner function in the lift would switch on
32.
by artagnon 4y ago
Is tree-sitter really slower than TextMate grammars? Some benchmarks indicate that this isn't really the case [1]. On the other hand, breaking parse trees is a real issue, because the error-recovery in tree-sitter is pretty rudimentary
33.
by artagnon 4y ago
Unfortunately, even the LLVM community has chosen a combination of Discord/Discourse, and deprecated their mailing list/IRC channel. This is a very unhealthy trend, and only the most ardent of communities such as Linux/Git&#x
34.
by artagnon 4y ago
Hehe, perhaps when I'm older. My collaborator on the LICS paper also tells me that the countryside is very beautiful. It will take time to get used to, as I've lived in big cities for the entirety of my life, and participate in ac
35.
by artagnon 4y ago
I initially kept that option open, yes. However, there are surprisingly few available positions in formal methods outside of academia, and Coq is very very hard: my ability to prove things with Coq is quite modest. Probably worth noting tha
36.
by artagnon 4y ago
It's less a question about what changes, and more a question about how well you can recall your past experience (I had the big picture, but forgot the details of several optimizations I'd written in the past, as well as certain CS
37.
by artagnon 4y ago
I used to work as a compiler engineer in the US for several years, before deciding to try starting over at the age of 30, in pure mathematics. I moved from the US to Paris in pursuit of an affordable mathematics education, and spent two yea
38.
by artagnon 4y ago
I think Lua was always seen as a bit obscure, and not enough people invested in the language to write useful utilities. It has a solid C foreign function interface, and the compiler is quite fast, which leaves me puzzled about why it never
39.
by artagnon 4y ago
It's interesting that Ruby now pulls Rust as a dependency, since YJIT is written in Rust [ https://github.com/ruby/ruby/tree/master/yjit ].
40.
Pylir – an MLIR-based AoT compiler for Python(github.com)
2 points by artagnon 4y ago|0 comments
41.
Firefly – an MLIR-based compiler and runtime for BEAM languages(github.com)
2 points by artagnon 4y ago|0 comments
42.
by artagnon 5y ago
Sorry to be the buzzkill here, but I'll say what needs to be said. Computers are decades away from being able to formalize any serious mathematical results, and "formalized mathematics" is a fancy term for "formal method
43.
by artagnon 6y ago
KaTeX doesn't do commutative diagrams, unfortunately.
44.
by artagnon 6y ago
Outputting beautiful designs is a function of the css, no? The bundled css is quite minimalist, and it comes packaged with a relatively simple starter website.
45.
by artagnon 6y ago
Yes, it's not the fastest ssg; there's Zola for that. However, digging git history with `git log --follow` can take a moment, and the MathJaX server-side rendering takes 10 seconds on a math-heavy site. However, incremental builds
46.
Show HN: Clayoven – beautiful website generator aimed at math-heavy sites(github.com)
115 points by artagnon 6y ago|26 comments
47.
by artagnon 6y ago
To formally verify simple things where a simple SMT solver does the job, why do you need a 40-year old beast like Coq? Even the very title of the article doesn't make much sense: why would you _want_ to translate Z3 to Coq? Coq is usef
48.
Integer Set Library: Study Notes(artagnon.com)
1 points by artagnon 6y ago|0 comments
49.
by artagnon 6y ago
Fwiw, I've lived in New York, Boston, and the Bay Area too. Four and a half years in the US in total ;)
50.
by artagnon 6y ago
Yes, this is the unfortunate reality. It happens to the best of software as it ages. The article doesn't address the elephant in the room: MediaWiki is really the _only_ solution to a difficult problem that we have today. Which other m
51.
No, the Singularity isn't coming – machine learning and common sense(artagnon.com)
4 points by artagnon 6y ago|1 comments
52.
by artagnon 6y ago
The choices are still available; it's just hidden beneath layers and layers of commoditization. Gone are the days when we could grow our own spices. Not really: you just have to move out of the city, to a nice European suburb and you c
53.
by artagnon 6y ago
I've experimented with Soylent for almost 1.5 years, and here are my main takeaways: 1. It's far from perfect, but can serve as a substitute for junk food. After six months of switching to Soylent, the cholesterol in my blood had
54.
by artagnon 6y ago
No, because my undergrad wasn't in math.
55.
by artagnon 6y ago
Chennai Mathematical Institute.
56.
by artagnon 6y ago
What seems to be the problem with CTRE?
57.
by artagnon 6y ago
Here are a couple of expertly-written C++17/C++20 repositories: https://github.com/hanickadot/compile-time-regular-expressio... https://github.com/nlohmann/json If you've not written C++
58.
by artagnon 6y ago
True. Examples are necessary for both motivation, and for showing how the formalisms work, at this level. One good undergraduate textbook that has plenty of examples is Dummit & Foote. However, that doesn't mean that you don't
59.
by artagnon 6y ago
Interesting approach. He starts off with vector spaces, after providing some intuition, and uses it to drive the rest of the book. He defines matrices in terms of linear maps, and talks about operations on vector spaces, with small sections
60.
by artagnon 6y ago
I'm not too fond of the example-driven approach. The student will certainly be able to multiply simple matrices and compute determinants in some simple cases, but will not be able to answer fundamental questions like "what can I p

More ›