<rss version="2.0" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:atom="http://www.w3.org/2005/Atom"><channel><title>Hacker News: burakemir</title><link>https://news.ycombinator.com/user?id=burakemir</link><description>Hacker News RSS</description><docs>https://hnrss.org/</docs><generator>hnrss v2.1.1</generator><lastBuildDate>Thu, 30 Apr 2026 08:38:34 +0000</lastBuildDate><atom:link href="https://hnrss.org/user?id=burakemir" rel="self" type="application/rss+xml"></atom:link><item><title><![CDATA[New comment by burakemir in "“Why not just use Lean?”"]]></title><description><![CDATA[
<p>A proof object in dependent type theory is just the term that inhabits a type. So are you saying the Lean implementation can construct proofs without constructing such a term?</p>
]]></description><pubDate>Mon, 27 Apr 2026 17:52:25 +0000</pubDate><link>https://news.ycombinator.com/item?id=47924915</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=47924915</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=47924915</guid></item><item><title><![CDATA[New comment by burakemir in "The seven programming ur-languages (2022)"]]></title><description><![CDATA[
<p>This article is full of gross mistakes. For example it claims that Caml is "Cambridge ML" which is ridiculously false. Fact check every sentence. Really sad.</p>
]]></description><pubDate>Sun, 19 Apr 2026 12:55:22 +0000</pubDate><link>https://news.ycombinator.com/item?id=47823959</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=47823959</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=47823959</guid></item><item><title><![CDATA[New comment by burakemir in "Microservices and the First Law of Distributed Objects (2014)"]]></title><description><![CDATA[
<p>You could build something like this using Mangle datalog. The go implementation supports extension predicates that you can use for "federated querying", with filter pushdown. Or you could model your dependency graph and then query the paths and do something custom.<p>You could also build a fancier federated querying system that combines the two, taking a Mangle query and the analyzing and rewriting it. For that you're on your own though - I prefer developers hand-crafting something that fits their needs to a big convoluted framework that tries to be all things to all people.</p>
]]></description><pubDate>Tue, 24 Mar 2026 12:40:45 +0000</pubDate><link>https://news.ycombinator.com/item?id=47501775</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=47501775</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=47501775</guid></item><item><title><![CDATA[New comment by burakemir in "Finding all regex matches has always been O(n²)"]]></title><description><![CDATA[
<p>I believe the technique described is similar to what I published here (this is not about all matches, but left-longest/shortest)<p>"Compiling regular expressions to sequential machines" (2005) ACM Symposium of Applied Computing <a href="https://dl.acm.org/doi/10.1145/1066677.1066992" rel="nofollow">https://dl.acm.org/doi/10.1145/1066677.1066992</a><p>(Note that there is a small mistake in the paper due to ambiguity, found by Vladimir Gapeyev. So the result does not hold in the generality stated but only for a special case when there is no ambiguity at "the end". There went my first PhD student publication...)<p>The two pass technique used to be implemented in the Scala compiler at the time (building DFAs upfront) , which could do regexps over lists and other sequences, but the approach would not work for top-down tree regexps so I did not pursue that and it got ripped out later.<p>It is good to see derivative regular expressions, Brzozowski/"position automata" used and discussed.</p>
]]></description><pubDate>Tue, 24 Mar 2026 12:21:12 +0000</pubDate><link>https://news.ycombinator.com/item?id=47501581</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=47501581</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=47501581</guid></item><item><title><![CDATA[New comment by burakemir in "Frankensqlite a Rust reimplementation of SQLite with concurrent writers"]]></title><description><![CDATA[
<p>Looks mildly interesting, but what's up with the license?<p>MIT plus a condition that designates OpenAI and Anthropic as restricted parties that are not permitted to use or else?</p>
]]></description><pubDate>Mon, 02 Mar 2026 05:40:42 +0000</pubDate><link>https://news.ycombinator.com/item?id=47214259</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=47214259</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=47214259</guid></item><item><title><![CDATA[New comment by burakemir in "Rust is just a tool"]]></title><description><![CDATA[
<p>A programming language is a medium to communicate programs to something that can execute them. That isn't exactly the same thing as a tool. A tool in my book is a metaphor for a program that helps achieve some well-defined task. Even if we ignore this difference, we would still want to talk about tool safety.<p>In my experience there is a C++ mob that hates Rust. These are the people who declare statement of facts as ideology. No good faith dialogue is possible.<p>There are also competent C++ programmers who misunderstand or don't know how static checking works.<p>I also witness normal people who are completely surprised by a statement like "C++ is all unsafe" and find that too strong.  Using the word "safe" with a technical meaning throws normal people off because, sadly, not everyone who writes code is an academic PL researcher.<p>"Safe", in Rust and much PL research, means "statically checked by the compiler to be free of UB". If you are pedantic, you need to add "... under the assumption that the programmer checked all conditions for the code that is marked `unsafe`" for Rust. That is all there is to it. Scientific definition.<p>C++ in its current form is full of gross design mistakes, many of which could be corrected at the price of breaking backwards compatibility. Mistakes happen, aldo to world leading PL researcher (the ML language and polymorphic references) which is why the field embraced mechanically checked proofs. The difference is the willingness to address mistakes.<p>Academics use "safe" in exactly the meaning the Rust community uses. If you don't understand this, go and educate yourself.
Academics need to communicate effectively which leads to technical meanings for everyday words or made up words and jargon.<p>Maybe a statically checked safe low-level language is marketing genius. It is also a technical breakthrough building on decades of academic research, and took a lot of effort.<p>Bjarne and friends chose a different direction. Safety was not a design goal originally but doubling down on this direction means that C++ is not going to improve. These are all facts.<p>Backwards compatibility is a constraint. Constraints don't give anyone license to stop people who don't have those constraints.<p>We don't have to feel any moral obligation to use statically checked languages for programs. But claiming that static checking does not make a difference is ignorant, and attaching value to one's ignorance certainly seems like an indicator for ideology and delusion.</p>
]]></description><pubDate>Sat, 28 Feb 2026 08:22:01 +0000</pubDate><link>https://news.ycombinator.com/item?id=47192196</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=47192196</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=47192196</guid></item><item><title><![CDATA[New comment by burakemir in "Show HN: Artifact Keeper – Open-Source Artifactory/Nexus Alternative in Rust"]]></title><description><![CDATA[
<p>Thanks for sharing.</p>
]]></description><pubDate>Fri, 06 Feb 2026 06:46:24 +0000</pubDate><link>https://news.ycombinator.com/item?id=46909867</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=46909867</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46909867</guid></item><item><title><![CDATA[New comment by burakemir in "Company as Code"]]></title><description><![CDATA[
<p>The approach described here - model things as graph - can really be applied to model any domains.<p>If you are into this type of modelling, you may find value in  Mangle, a datalog-based logic programming language and deductive database library. You do not need to invent dozens of DSLs but can do it all in one. And without all the RDF trouble.<p><a href="https://github.com/google/mangle" rel="nofollow">https://github.com/google/mangle</a><p>HN discussion <a href="https://news.ycombinator.com/item?id=33756800">https://news.ycombinator.com/item?id=33756800</a><p>Talk at REBASE 2025 "From Facts to Theories" <a href="https://youtu.be/UjOEHSZDBH8?si=qAjnkBQfPKMVaOPW" rel="nofollow">https://youtu.be/UjOEHSZDBH8?si=qAjnkBQfPKMVaOPW</a></p>
]]></description><pubDate>Thu, 05 Feb 2026 19:58:22 +0000</pubDate><link>https://news.ycombinator.com/item?id=46904327</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=46904327</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46904327</guid></item><item><title><![CDATA[New comment by burakemir in "The only moat left is knowing things"]]></title><description><![CDATA[
<p>You're absolutely right.</p>
]]></description><pubDate>Thu, 29 Jan 2026 10:44:05 +0000</pubDate><link>https://news.ycombinator.com/item?id=46808342</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=46808342</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46808342</guid></item><item><title><![CDATA[New comment by burakemir in "Linux Sandboxes and Fil-C"]]></title><description><![CDATA[
<p>My trouble with separate categories "memory safety technology" and "sandboxing technology" is that something like WASM execution is both:<p>* Depending on how WASM is used, one gets safety guarantees. For example, memory is not executable.<p>* Privileges are reduced as a WASM module interacts with the environment through the WASM runtime and the embedder<p>Now, when one compiles C to WASM one may well compile things with bugs. A memory access bug in C is still a memory access bug, but its consequences can be limited in WASM execution. Whether fail-stop behavior is guaranteed actually depends on the code the C compiler generates and the runtime (allocation/deallocation, concurrency) it sets up.<p>So when we enumerate immediately available security options and count WASM as sandboxing, this is not wrong. But WASM being an execution environment, one could do a lot of things, including a way of compiling and executing C that panics when a memory access bug is encountered.</p>
]]></description><pubDate>Sun, 14 Dec 2025 03:12:56 +0000</pubDate><link>https://news.ycombinator.com/item?id=46260471</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=46260471</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46260471</guid></item><item><title><![CDATA[New comment by burakemir in "Typechecking is undecideable when 'type' is a type (1989) [pdf]"]]></title><description><![CDATA[
<p>"A Polymorphic λ-calculus with Type:Type"</p>
]]></description><pubDate>Sun, 23 Nov 2025 20:41:01 +0000</pubDate><link>https://news.ycombinator.com/item?id=46027138</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=46027138</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46027138</guid></item><item><title><![CDATA[New comment by burakemir in "Typechecking is undecideable when 'type' is a type (1989) [pdf]"]]></title><description><![CDATA[
<p>I remember a Luca Cardelli paper that explores a language with  "type:type" and it contains a sentence roughly expressing: "even if the type system is not satisfying as a logic, it offers interesting possibilities for programming"</p>
]]></description><pubDate>Sun, 23 Nov 2025 17:55:30 +0000</pubDate><link>https://news.ycombinator.com/item?id=46025724</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=46025724</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=46025724</guid></item><item><title><![CDATA[New comment by burakemir in "Learn Prolog Now (2006)"]]></title><description><![CDATA[
<p>Learn Datalog Now!</p>
]]></description><pubDate>Thu, 13 Nov 2025 08:06:30 +0000</pubDate><link>https://news.ycombinator.com/item?id=45912113</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=45912113</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45912113</guid></item><item><title><![CDATA[New comment by burakemir in "Memory Safety for Skeptics"]]></title><description><![CDATA[
<p>Did you read what I wrote up there?<p>There is art and there is science. What both have in common is that their protagonists do not intend to become obstacles of progress.<p>I'm afraid GC'd languages have been around for a very long time and yet we continue to talk about memory safety as an urgent problem. Now what?<p>How does pretending that low-level memory safety is not its own complex domain deserving of its own technical definitions help with anything?</p>
]]></description><pubDate>Tue, 11 Nov 2025 22:03:34 +0000</pubDate><link>https://news.ycombinator.com/item?id=45893506</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=45893506</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45893506</guid></item><item><title><![CDATA[New comment by burakemir in "Memory Safety for Skeptics"]]></title><description><![CDATA[
<p>This is a false dichotomy. Language design choices are the causes of security and software vulnerabilites. It is possible to recognize the value of GC languages and have precise technical terminology at the same time. We can invent new words.<p>I believe everyone who cares about memory safety appreciates that certain bugs cannot occur in Java and go, and if the world calls that memory safe, that is ok.<p>There are hard, well-defined guarantees that a language and implementation must make, and a space of trade-offs. We need language and recognition for the ability to push the boundary of hard, well-defined guarantees further. That, too, is memory safety and it will be crucial for moving the needle beyond what can be achieved with C and C++.<p>No one has a problem with applications being ported from low-level to GC-ed languages, the challenge is the ones where this is not possible. We need to talk about memory safety in this specific context, and mitigations and hardening will not solve the entire problem, only pieces of it.</p>
]]></description><pubDate>Tue, 11 Nov 2025 08:05:04 +0000</pubDate><link>https://news.ycombinator.com/item?id=45885113</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=45885113</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45885113</guid></item><item><title><![CDATA[New comment by burakemir in "Memory Safety for Skeptics"]]></title><description><![CDATA[
<p>This is a good article.<p>Small nit: As someone curious about a definition of memory safety, I had come across Michael Hicks' post. He does not use the list of errors as definition, and argues that such a definition is lacking rigor and he is right. He says;<p>> Ideally, the fact that these errors are ruled out by memory safety is a consequence of its definition, rather than the substance of it. What is the idea that unifies these errors?<p>He then offers a technical definition (model) involving pointers that come with capability of accessing memory (as if carrying the bounds), which seems like one way to be precise about it.<p>I have come to the conclusion that language safety is about avoiding untrapped errors, also known as "undefined behavior". This is not at all new, it just seems to have been forgotten or was never widely known somehow. If interested, find the argument here <a href="https://burakemir.ch/post/memory-safety-the-missing-def/" rel="nofollow">https://burakemir.ch/post/memory-safety-the-missing-def/</a></p>
]]></description><pubDate>Mon, 10 Nov 2025 21:40:56 +0000</pubDate><link>https://news.ycombinator.com/item?id=45881311</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=45881311</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45881311</guid></item><item><title><![CDATA[New comment by burakemir in "Swiss voters back e-ID legislation"]]></title><description><![CDATA[
<p>Finally a good use case for decentralized technology? From <a href="https://www.eid.admin.ch/en/technology" rel="nofollow">https://www.eid.admin.ch/en/technology</a>
"The e-ID architecture is based on a decentralised identity model that gives users full control over their identity and personal data. There is no central authority that aggregates, stores or controls credentials. Data flows occur directly and in a decentralised manner between the holder and an issuer or verifier. Linkability of usage across different services is technically restricted. Interactions between different actors also cannot be directly linked. During a verification process, the holder shares only the necessary data directly with a verifier, without the issuer being informed."</p>
]]></description><pubDate>Sun, 28 Sep 2025 21:12:34 +0000</pubDate><link>https://news.ycombinator.com/item?id=45408061</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=45408061</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45408061</guid></item><item><title><![CDATA[New comment by burakemir in "Claude can sometimes prove it"]]></title><description><![CDATA[
<p>There is a place for informal, prose specs, and I can easily agree that more people are nowadays describing their programs in English.<p>The context here is formal specs though - adequately and precisely capturing the intended meaning (semantics) in a way that lends itself to formal verification.<p>Interactive theorem proving is interactive because proof search is intractable; a human articulates the property they want to prove and then performs the "search". Apart from the difficulties of getting to that proof, it can also happen that all goes through and you realize that the property is not exactly what you wanted.</p>
]]></description><pubDate>Sat, 20 Sep 2025 12:31:27 +0000</pubDate><link>https://news.ycombinator.com/item?id=45312797</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=45312797</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45312797</guid></item><item><title><![CDATA[New comment by burakemir in "Claude can sometimes prove it"]]></title><description><![CDATA[
<p>I will quote (approximately) Simon Peyton Jones: "writing programs is not hard. Specifying what a program should do is hard."<p>Prove what? The author is well versed in the problem of specifications as the aliens-demand-gcc-correctness-or-else post. I also enjoyed the other post where they say "no one cares about correctness" and "people care about compliance".<p>It is safe to say, most people are not experts and will never become experts.<p>Being proficient in the business of coming up with suitable specification that can be implemented and getting assurance that an implementation meets the spec will most likely need all the kind of formal training for humans that the AI hype industry assures us is no longer necessary.<p>So it doesn't much help that LLMs are good at manipulating the tokens when used by experts, at least not in a big way. It can be hoped that they change cost-benefit balance in good ways, but the bigger problems of the industry will simply persist.<p>What would need to change for a more fundamental shift is getting a lot more people to understand the value of specifications. This is an education problem and paradoxically I could see AI helping a lot... if only there was enough interest in using AI to help humans become experts.</p>
]]></description><pubDate>Sat, 20 Sep 2025 11:35:35 +0000</pubDate><link>https://news.ycombinator.com/item?id=45312424</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=45312424</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45312424</guid></item><item><title><![CDATA[New comment by burakemir in "Safe C++ proposal is not being continued"]]></title><description><![CDATA[
<p>There is an old definition of language safety which means "no untrapped execution errors". It is not the only way to define safety, but it is a good way that you can adapt to various kinds of x-safety, such as memory safety.<p>I have a little post that explains this using a few more words, if interested:
<a href="https://burakemir.ch/post/memory-safety-the-missing-def/" rel="nofollow">https://burakemir.ch/post/memory-safety-the-missing-def/</a></p>
]]></description><pubDate>Sun, 14 Sep 2025 19:36:27 +0000</pubDate><link>https://news.ycombinator.com/item?id=45242603</link><dc:creator>burakemir</dc:creator><comments>https://news.ycombinator.com/item?id=45242603</comments><guid isPermaLink="false">https://news.ycombinator.com/item?id=45242603</guid></item></channel></rss>