derkha

6 ms·

1.
by derkha 12d ago
No, comparator does check the entire closure
2.
by derkha 3y ago
The tower was built after Brahe's death https://www.rundetaarn.dk/en/article/tycho-brahe-was-not-her...
3.
by derkha 5y ago
Insignificant consequences. https://www.fiercehealthcare.com/hospitals/how-many-employee...
4.
by derkha 6y ago
Lean 4 developer here. If the array is shared, we make a full copy. It's the same semantics as in Swift.
5.
by derkha 6y ago
I believe the reasoning is that aerosol would have ultimately spread everywhere, including on the AC itself, while ballistics can be heavily influenced by airflow, but are still limited in range.
6.
by derkha 6y ago
They probably mean "red-yellow", which is an intermediate "wait for it" state in many European countries, including Germany https://de.wikipedia.org/wiki/Ampel#/media/Datei:Traffic_lig...
7.
by derkha 7y ago
Reading through https://bazel.build/designs/skyframe.html , this sounds pretty much like what would be possible with the aforementioned recursive Nix and content-addressed paths. Bazel might still win in practice since
8.
by derkha 7y ago
I prefer the simplicity of https://github.com/firecat53/networkmanager-dmenu , which works fine under sway
9.
by derkha 7y ago
Implementation on Github: https://github.com/microsoft/mimalloc
10.
by derkha 8y ago
You can convert a `String` into a `&'static str` using only safe stdlib functions via `Box::leak(s.into())`. This uses `unsafe` internally, of course... but so does almost any code.
11.
by derkha 10y ago
Yes, that is a valid alternative encoding: https://en.wikipedia.org/wiki/Church_encoding#Represent_the_... In general, what you describe is representing an inductive type by its _eliminator_: https://www.quo
12.
by derkha 10y ago
Author of that project here, it's the other way around - I'm using the absence oft aliasing to turn mutable Rust code immutable, which I can then embed in Lean. But you're right that ownership (ie, affine types) per se doesn&
13.
by derkha 10y ago
What would that abstraction look like? I really can't think of a more high-level abstraction of parallelism than a single method call saying "Please parallelize this sequential algorithm. But only when it makes sense."
14.
by derkha 10y ago
What do you mean by "turning into"? I don't see much special syntax in the post apart from the general expression-oriented functional style, including higher-order functions. Which has always been part of Rust. If that means
15.
by derkha 10y ago
> 1.16699016 × 10-8 hertz IOW, once every 2.7 years. Google Calculator is genius.
16.
by derkha 10y ago
Nice, this may make me finally move on from irssi
17.
Observational Equivalence and Unsafe Code(smallcultfollowing.com)
4 points by derkha 10y ago|0 comments
18.
by derkha 10y ago
Aside from program synthesis, there is the more restricted form of code extraction , which turns definitions inside a theorem prover into code in a more traditional, runnable language such as OCaml. But you'll still want to do one or
19.
by derkha 10y ago
But widgets do have the same type: Widget, which the author already uses as a trait object. I think he was getting confused by mixing &Widget and Rc<RefCell<Widget>>. Just declare a type alias for the latter, use it everywhe
20.
by derkha 10y ago
I actually started the project in Isabelle: https://github.com/Kha/electrolysis/tree/isabelle/thys . Automation was nice, translating Rust traits not so much. You really want them to be type classes, whic
21.
by derkha 10y ago
I have heard of it, it features a nice application of Separation Logic. Though not needing that kind of logic at all does feel even better! There is also an extension of an extension of CFML to asymptotic complexity analysis, after which I
22.
by derkha 10y ago
Well, that change would also break the proof in general :) . But I see your point. I've written about overflow checking some more below, but what you'd really want for that is some solid support of subtypes or refinement types - i
23.
by derkha 10y ago
By calling the verification 'simple' myself, I concede that it may also be _simplistic_ in parts. Perhaps I should have emphasized that this project is mostly about algorithmic correctness currently. A bug in the compiler backend
24.
by derkha 10y ago
There is a PR for a Lean backend producing both C++ and Rust: https://github.com/leanprover/lean/pull/1090 Note, however, that this is purely focused on executing Lean code, not integrating with other C++&#x2
25.
by derkha 10y ago
Even the EU seems to think so: http://www.reuters.com/article/us-turkey-security-eu-hahn-id...
26.
by derkha 10y ago
To clarify Bahamut's point: The functions must be analytic - https://en.wikipedia.org/wiki/Analytic_continuation#Initial_... . Regardless of the actual value of foo, at least one of g or h won't be differentia