Viewing profile — derkha

The tower was built after Brahe's death https://www.rundetaarn.dk/en/article/tycho-brahe-was-not-her...

Insignificant consequences. https://www.fiercehealthcare.com/hospitals/how-many-employee...

Lean 4 developer here. If the array is shared, we make a full copy. It's the same semantics as in Swift.

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 li…

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…

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. B…

I prefer the simplicity of https://github.com/firecat53/networkmanager-dmenu , which works fine under sway

Implementation on Github: https://github.com/microsoft/mimalloc

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…

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 _e…

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 th…

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 alg…

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…

> 1.16699016 × 10-8 hertz IOW, once every 2.7 years. Google Calculator is genius.

Nice, this may make me finally move on from irssi

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 langu…

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 >. Just declare a type alias fo…

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 …

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 extensi…

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…

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 cor…

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 in…

Even the EU seems to think so: http://www.reuters.com/article/us-turkey-security-eu-hahn-id...

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 o…