xavxav

14 ms·

91.
by xavxav 4y ago
OCaml is an impressive language on many fronts: compile time, speed, memory usage, but then is almost crippled beyond usage by a few unfortunate decisions / (lack of) features: - Dependency management, despite progress `opam` is hopele
92.
by xavxav 4y ago
> INRIA university tiny nit, but INRIA is not a university but rather a national network of labs.
93.
by xavxav 4y ago
Yea but it’s not really useable in practice as it heavily relies on nesting allocations in closures to simulate “generative lifetimes”. It’s a research artifact, not meant for serious usage. Instead, I would recommend using something like
94.
by xavxav 4y ago
I agree that debugging bad macros is annoying, especially proc-macros but that’s not comparable since by their very nature proc macros are no more powerful than hand written code. They cannot create new semantics, at best they can add new s
95.
by xavxav 4y ago
An immediate issue which could be addressed with further complexity is that for loop desugaring is done very early in Rust's compilation pipeline, way before typing is actually performed. This would also be weird in the case that you
96.
Rust stabilizes generic associated types(github.com)
152 points by xavxav 4y ago|52 comments
97.
by xavxav 4y ago
But they have, we wouldn’t be able to design, build or operate those 100M machines without plenty of cutting edge micro-electronics at every step of the way. When you look at the details of how these machines are made, the price tag almost
98.
by xavxav 4y ago
Today you help finance someone’s fiber, tomorrow they help finance your hospital/fire dept/etc, that’s the whole idea of public works.
99.
by xavxav 4y ago
I don’t get what is meant by clever in this context, how do you “cleverly” introduce yourself by writing to someone? I do agree with the broader point about cleverness’ failure mode though.
100.
by xavxav 4y ago
In France, you normally can't apply for a thesis without funding (it may vary on field though). And the moment you have funding that makes you an employee, with the protections accorded. Since most theses are funded using public money,
101.
by xavxav 4y ago
It also depends on where you did your thesis in the first place. The UK has stronger protections for grad students than the US (not hard to do). In any case it shouldn't be up to whether you had a permissive advisor or not, PhD student
102.
by xavxav 4y ago
The visualization that works for me is to imagine the surface of a balloon as a 2D universe. As you inflate the balloon it stretches out despite the skin having no “center” to speak of.
103.
by xavxav 4y ago
I can’t overstate the value of the lunch hour in France, it’s by far the best part of my day and has made my PhD bearable, enjoyable even despite the difficult pandemic environment. It’s allowed me to learn from colleagues, make friends and
104.
by xavxav 4y ago
Check out Sarek’s thesis in the evaluation section: https://sarsko.github.io/_pages/SarekSkotåm_thesis.pdf . In general it’s roughly at the level of microsat so worse than minisat and kissat, but not garbage either.
105.
by xavxav 4y ago
Indeed, Creusot itself is not formally verified, but we have verified the metatheory in our paper RustHornBelt: https://people.mpi-sws.org/~dreyer/papers/rusthornbelt/paper... . Actually verifying the transla
106.
by xavxav 4y ago
SAT comp gives you 5x the solving time to check your proof, which is indicative that checking isn’t so simple (though it is on paper)
107.
by xavxav 4y ago
Hi! I’m the author of Creusot, Sarek did some amazing work on CreuSAT, he also had to teach himself formal verification and SAT solving along the way. If you have any questions about CreuSAT or Creusot, I’d be happy to answer
108.
by xavxav 4y ago
> Is the Async crew mostly writing web servers and other things that operate using TCP and HTTP? Lower level (eg IP, Eth, network hardware drivers) isn't well supported by rust libs. Nor is higher - we have Flask analogs, but no Dja
109.
by xavxav 4y ago
Honestly, to me this project is a means seeking an end, the same way JS devs love to play around with frontend frameworks, the author saw a bunch of shiny powerful (highly complex) tools and decided that combining them all was the solution
110.
by xavxav 4y ago
If you're interested by this, you might also like recent work I participated in developing RustHornBelt, which allows reasoning about the functional correctness of Rust code, and will be published at PLDI'22 in June. Our preprin
111.
by xavxav 4y ago
> It could be baked into proof assistants that are part of (optional or add-on) tooling, like what sel4 does. A simpler language makes this more possible, and the things that a proof assistants can do go far beyond what rust is able to p
112.
by xavxav 4y ago
> Yes. Glidesort moves data back and forth between partially initialized buffers a lot, so unsafe code is unavoidable. I also need to concatenate slices that are adjacent in memory, which is impossible to do with safe slices (due to poin
113.
by xavxav 4y ago
>I have to still do some extra correctness vetting and testing, and in particular exception-safety is still not yet fully implemented. This is important because I wrote it in Rust where we must always give back a valid initialized array,
114.
by xavxav 5y ago
I would argue it’s language-ub to convert an invalid slice into into a String, it’s bubbling up a requirement of str which relies on the contained utf-8 to be well-formed for memory safety.
115.
by xavxav 5y ago
I’m doing my PhD on the formal verification of Rust, and while you’re right that safe code provides a lot of informal advantages it also dramatically simplified form reasoning. In particular, the dirty secret of C verifiers is that they don
116.
by xavxav 5y ago
Sure, but as I'm sure you're aware, the current system makes this model impossible for all but the most niche products: a faster growing, better funded (because they are growing faster) product will outspend you until you die. The
117.
by xavxav 5y ago
Well, GDPR fines are ramping up over time, regulators seem to have been easing companies into it rather than starting off with the 10B fines from day 1. I still hope to see some serious fines on FB / Google in the coming years.
118.
by xavxav 5y ago
The manuscripts weren't in Greece. These works were written centuries ago, many of them before the rise of the roman empire. As books were expensive back then, they would often be found in wealthy cities like Rome, Alexandria or Cons
119.
by xavxav 5y ago
I’m happy that they finally released this monitor, it felt weird that you could get an imac which was sleeker than any existing screen, but does anyone know of more affordable alternatives? This may be a bit weird/niche but I care a l
120.
New wiper malware being used in attacks on Ukraine(twitter.com)
1 points by xavxav 5y ago|0 comments

More ›