burakemir

A definition of memory safety without data race freedom may be more precise but arguably less complete.

It is correct that data races in a garbage collected language are difficult to turn into exploits.

The problem is that data races in C and C++ do in fact get combined with other memory safety bugs into exploits.

A definition from first principles is still missing, but imagine it takes the form of "all memory access is free from UB". Then whether the pointer is in-bounds, or whether no thread is concurrently mutating the location seem to be quite similar constraints.

Rust does give ways to control concurrency, eg via expressing exclusive access through &mut reference. So there is also precedent that the same mechanisms can be used to ensure validity of reference (not dangling) as well as absence of concurrent access.

Two big differences:

  - it is typed, and

  - multi-stage programming can also describe runtime-code generation.

Enjoyed this, but looking at these from manager decision scenario is of course going to bias towards the more subjective.

For a different scenario, imagine you operate a large distributed system and have been paged at 3 am because there is a problem. Besides taking steps to contain the fallout, you want to quickly locate the error and take steps to prevent this stuff from ever happening again.

Unlike a hiring decision, you want to propose measures such that a large number of people get to agree that the state of affairs will improve. It is a truism that we don't want software to fail, so considering expectations may not necessarily help here, and rationality would suggest to strive to achieve an "objective" improvement - and one that does not make the system harder to understand or invite new, different failures.

So all in all, I enjoyed this advocacy of Tellman's perspective, but it does not always seem appropriate to apply it and more meta than the others.

I made some progress porting mangle datalog to Rust https://github.com/google/mangle/tree/main/rust - it is in the same repo as the golang implementation.

It is slow going, partly since it is not a priority, partly because I suffer from second system syndrome. Mangle Rust should deal with any size data through getting and writing facts to disk via memory mapping. The golang implementation is in-memory.

This post is nice because it parses datalog and mentions the LSM tree, and much easier to follow than the data frog stuff.

There are very many datalog implementations in Rust (ascent, crepe) that use proc-macros. The downside is that they won't handle getting queries at runtime. For the static analysis use case where queries/programs are fixed, the proc macro approach might be better.

Common Table Expression, a SQL concept that enables more expressive programming with SQL queries. They are introduced using WITH ...

One angle (no static types) is racket, which knows multiple stages for its macros. Maybe the most developed actually working "new tradition".

Researchers have also looked into multistage programming, which is enabled by representing code at runtime. Including how to represent it in type systems/logic.

For Scala, there was a realization that both macros and multistage programming need a representation of programs. I am falling asleep so can't dig out references now, but it is exciting stuff and I think the last word has not been written on all this.

It is consistent with the way the Rust community uses "safe": as "passes static checks and thus protects from many runtime errors."

This regularly drives C++ programmers mad: the statement "C++ is all unsafe" is taken as some kind of hyperbole, attack or dogma, while the intent may well be to factually point out the lack of statically checked guarantees.

It is subtle but not inconsistent that strong static checks ("safe Rust") may still leave the possibility of runtime errors. So there is a legitimate, useful broader notion of "safety" where Rust's static checking is not enough. That's a bit hard to express in a title - "correctness" is not bad, but maybe a bit too strong.

In an attempt to get a more general version of a debt metaphor, let's look at ingredients: - there is a time interval - we have a utility function, or at least desire one or want to pretend we have one - there is a decision - there is uncertainty

From here there are many paths...

"Deliberate vs inadvertent" describes whether we know about the effect the decision has on the utility function.

"Reckless vs prudent" describes whether we are rational and realize that decisions have consequences.

It is also possible that we don't actually have a utility function. Or different people involved in the decision have different utility functions or don't feel the same responsibility towards the outcome (not unheard of when it comes to maintenance/design/architecture vs feature).

What makes the debt metaphor very attractive is that it evokes an image of being in control. We may not have spelled out the utility function but everyone agrees it is bad now so we can pretend it was a rational choice we had. The alternative that we did not take any decision when we could have or were too distracted to see the consequences is much harder to accept. So now that we have debt, let's talk about whether we choose to pay it back or now.

Rather than working hard to create this faux image of control, I wonder how often teams may be better off having an honest discussion about what the utility function is or should be, which decisions will make the group move in the right direction and how the team can keep oneself accountable that the effects that one had in mind actually took place.

Hi Steven, I will check it out.

What I like about Cardelli's handbook article is how he lays down type systems in programming languages as its own thing. This is inspired by logic but definitely not the same - just as mathematical logic can well be called the origin of programming languages and PL semantics but then there is so much knowledge, difference in purpose and practical concerns that separate the two fields.

From a quick glance at the article, this looks like an interesting linguistic exploration into terminology around "type". It is questionable that such an approach is ultimately effective at getting us closer to a standard meaning, but the author is arguing well that there are sometimes subtle and sometimes not so subtle differences in our various uses of the word "type" and "type system".

Consider how it could be seen as a bit disappointing how the author goes to all these lengths with "type" and then deals with "memory safety" by merely repeating the often repeated tags "spatial" and "temporal" which is missing phenomena like corruption through unrestricted concurrent access or other memory model aspects.

It seems that coming up with a complete ontology that would capture all nuance is going to be out of the question and not how technical language works. Rather, technical definitions can be made to work within a well defined scope, which leaves enough room for everyday language to be vague. The question is then what level of generality we want to shoot for.

I found Luca Cardelli's definitions in his CRC handbook of computer science and engineering article very helpful - these are "type discipline" uses of the word which the OP already finds coherent. http://lucacardelli.name/Papers/TypeSystems.pdf

Dependent types typically refers to type systems where a type can depend on a term. The canonical example is "Vector n" where n is some expression that evaluates to a natural number.

Refinement types typically(1) refers to a type systems that lets you create a subtype of a type through refining (qualifying) with a predicate or constraint on the shape. Examples {x \in int | is_even x } or { x \in List | len(x) = 1 }

Refinement types can be very powerful but that may well make type checking undecidable (think of a type of Turing machines, and the refinement that keeps only the ones that halt). By being careful about the logic used in the refinements, one may retain decidability.

(1) The article seems to have a different idea of what a refinement type is: quote "a type system that does its work after another type system has already done its work".

I am not going to play orthodox guardian of type theory terminology here, yet to me personally, it does seem unfortunate to use that term. The author seems to really want a form of type-level computation, which could be interesting if it could be rigorously specified and it's relation to the existing type level reduction clarified.

Agreed. The large and passionate community may have multiple factors but "things actually work" is probably a factor.

It is hard to get a full picture of how academic research influenced Rust and vice versa. Two examples:

- The use of linearity for tracking ownership in types has been known to academics but had never found its way into a mainstream language.

- researchers in programming language semantics pick Rust as a target of formalization, which was only possible because of design choices around type system. They were able to apply techniques that resulted from decades of trying to get a certified C. They have formalized parts of the standard library, including unsafe Rust, and found and fixed bugs.

So it seems fair to say that academic research on safety for C has contributed much to what makes Rust work today, and in ways that are not possible for C and C++ because these languages do not offer static guarantees where types Transport information about exclusive access to some part of memory.

In other words: you encode them. That is likely also the reason why many programming languages did not have sums. You have something else that can be used similarly.

A sum type is a disjoint union so a straightforward encoding of A+B would be (tag:bool, A?, B?) in made-up syntax. When tag==0 then A is present When tag==1 then B is present

On a different level, the fact that a column can be NULL itself can be considered a sum, like A? = A + {NULL}.

Not bad, an article aiming to popularize product and sum types. I am not the target audience, but wished there was a way to get the masses to understand that elementary type theory and logic are at the heart of these programming concepts that remain the same across languages.

Back when I worked on translation of pattern matching in the Scala compiler (pre Kotlin, pre "Java 5" with generics..) I surely hoped but could not imagine that the world would turn out like this, with python, Java, Rust all supporting matching and sum types.

I don't see many texts that bridge type theory (mathematical logic) and data modeling, but I am certainly rooting for sum and product types to become pervasive common knowledge to all programmers one day.

Generics are a powerful mechanism, and there is a spectrum. The act of retrofitting generics on go without generics certainly meant that some points in the design space were not available. On the other hand, when making a language change as adding generics, one wants to be careful that it pulls its own weight: it would be be sad if generics had been added and then many useful patterns could not be typed. The design choices revolve around expressivity (what patterns can be typed) and inference (what annotations are required). Combining generics with subtyping and inference is difficult as undecidability looms. In a language with subtyping it cannot be avoided (or the resulting language would be very bland). So I think the answer is no, this part of the complexity could not have been avoided. I think they did a great job at retrofitting and leaving the basic style of the language intact - even if I'd personally prefer a language design with a different style but more expressive typing.

The Mangle repo has the beginnings of a Rust implementation but it will take some time before it is usable. The go implementation is also still being improved, but I think real DB work with persistent data will happen only in Rust. Bindings to other host languages would also use the Rust implementation. There are no big challenges here it is just work and takes time.

The combination of top-down and bottom up logic programming is interesting, especially when one can move work between pre computation and query time.

I like that optimizing queries in datalog can be discussed like optimization of programming language but of course the biggest gains in DB come from join order and making use of indices. There is a tension here between declarative and having some control or hints for execution. I haven't yet figured out how one should go about it, and also how to help programmers combine top-down and bottom-up computation. Work in progress! :-)

Here is a proof that you can translate non-recursive datalog into relational algebra and vice versa: https://github.com/google/mangle/blob/main/docs/spec_explain...

Since Logica is translated to SQL it should benefit from all the query optimistic goodness that went into the SQL engine that runs the resulting queries.

I personally see the disadvantages of SQL in that it is not really modular, you cannot have libraries, tests and such.

Disclosure: I wrote Mangle (the link goes to the Mangle repo), another datalog, different way of extending, no SQL translation but an engine library.

"In summary, it is highly misleading to suggest that Microsoft (or ICOMP) initiated or in any way controlled Foundem’s European complaint or any of Foundem’s other initiatives." Source: http://www.searchneutrality.org/uncategorized/foundem-is-not...

I am sure Clojure is great but it really shows the need for an "overview of datalog" that is not embedded in the context of a programming language with it's own syntactic choices.

My own humble attempt is here https://github.com/google/mangle ... I had come across datalog in Clojure and thought it is a complete nonstarter. Most people (including me) are not in a position to start using Clojure if all they want is a query capability.

IMHO what most people would want a datalog implementation that is very easy to integrate into their existing setup, with their existing data. Yet for extensibility it is also important to enable users to write datalog queries in it's own special syntax so one can have type checking, modules, declarations in a way that is independent of the host programming language.

From a teaching point of view, one does need an example database. Here is "employee department boss", with a volunteering spin: https://github.com/google/mangle/blob/main/docs/example_volu...

There is a long history of approaches to integrate querying into programming languages (eg LINQ). Trade off here between making an easy to use yet powerful query language, keeping it simple and integrating it tightly into the host language or using a DSL along clear interface.

In addition to labelled property graphs and triples, a list of approaches to knowledge graph should consider facts(tuples) that are connected via common values as a form of graph, with datalog queries to query them. This is a lot more flexible than either approach IMHO and also more easily connected to existing relational data.

RDFox is a tool that uses Datalog internally. RelationalAI uses a datalog based approach. Another example is Mangle Datalog, my own humble open source project that can be found on GitHub.

The language in the article about relational being "non native graph" is a bit biased. With some developer attention, there are massive opportunities to store data in a distributed manner and with te right indices querying can be fast. Though to be fair, good performance will always need developer attention.

For the subproblem of being able to unify and query various data sources in different formats, I would suggest to take a look at Datalog and specifically Mangle, my implementation of it. I don't want to plug the project here but more describe the approach.

Usually your data will comfortably fit in a file. Your data getter emits these files in facts (essentially relations). If you want structures data, it can also be a single column that is of some struct type (similar to protobuf).

With all data available the problem becomes one of querying. With a good enough query language and system, you write these can data transformations via Datalog rules which roughly correspond to database views.

It is always possible to write queries in code in a general purpose language, but is a bit clumsy and hard to get an overview or reuse. It may also be possible to do SQL but it SQL is not very compositional and you ask yourself whether the base data representation should be adapted refactored. Essentially you do not want to think about the optimal schema or set of structs but just do transformations you need in the lowest friction way.

With Datalog you may benefit from a unified representation (everything is "facts") and the transformations to useful different formats (different kinds of facts) can be factored and reused. It may mean duplication and denormalization but usually that does not matter.

Mangle supports aggregation and even calling some custom functions during query evaluation. The repo is at https://github.com/google/mangle and obviously there remains a lot to do, the API is unstable, there are bugs and the type checker is not finished... but a number of people and projects seem to use it. Even if you do not use it, it may give you how to use facts (relations) as a unified data structure for your project.

Interesting! IIUC this is done using source-to-source translation? It is a bit hard to understand from the docs what technical approach is. The docs are clearly aimed at users and I find them impressive, well done. I'd be interested in knowing the approach and how it compares to wasm based Rust web frameworks before diving more deeply into it.

One advantage of combining Rust with Flutter seems to be that Flutter is a whole framework already and one would be able to share code and data structures between server and client side.

A comparison with other ways Rust

Really appreciate the bits in the article about identifying what is fundamental and correcting misevaluations.

Making an outline is also important for writing. However doing research also has its place. See this here https://cse.buffalo.edu/~rapaport/howtostudy.html#makeoutlin... (also previously discussed on HN)

Let's define a mapping F to act as a "signature-step" of an algebraic data type with operations op as a map (functor) from X to Sum_op X^arity(op).

This involves a sum of products (or coproduct of products). See "Recursive types for free" https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/f...

Mangle is a language that includes "textbook datalog" as a subset https://github.com/google/mangle ; like any real-world datalog language, it extends datalog with various facilities to make it practical.

It was discussed on HN https://news.ycombinator.com/item?id=33756800 and is implemented in go. There is the beginnings of a Rust implementation meanwhile.

If you are looking for datalog in the textbooks, here are some references: https://github.com/google/mangle/blob/main/docs/bibliography...

A graph DBs short intro to datalog: just like the edges of a graph could be represented as a simple table (src, target), you could consider a database tuple or a datalog or prolog fact foo(x1, ..., xN) as a "generalized edge." The nice thing about datalog is then that as one is able to express a connections in an elegant way as "foo(...X...), bar(...X...)" (a conjunction, X being a "node"), whereas in the SQL world one has to deal with a clumsy JOIN statement to express the same thing.

Negation is not all that well understood even in formal settings.

When PROLOG introduced negation-as-failure, many logicians (Girard) were repulsed: how can failure to find a proof for a proposition P be considered a proof of the negation (not P)? Yet there are theories where this just "works" because P is about some inherently finite set of observations (not (John Doe is an employee)) is very much the failure of finding a record after consulting the employee database.

The different treatment of negation in intuitionistic logic and classical logic is another example. Intuitionistic logic is more precise than classical: a statement of classical logic logic can be translated into one of intuitionistic logic (eg Gödel-Gentzen) that is provable if and only if the original statement was provable.

Things like identity, equality, negation in real life reasoning seem to often be "good enough"/ fuzzy rather than rigorous applications of logic.

There are people who argue that after the horrible events of the 20th century, the time has come to stop pretending that science could be an "objective" universal pursuit of truth and accept that it's results can at any point in time become an instrument of power and thus subject to forces that pursue benefits for less than all of humanity. I have not read much more than TFA but both points of view, Musk's and LeCun's seem to be missing this perspective completely. In a philosophy of science, it seems hardly enough to describe how a group of people is to pursue knowledge. It also matters what then happens with that knowledge.

It is often assumed that publishing would somehow automatically ensure access and the option of benefiting from that knowledge, however there are many examples where this is not so.

I like this way of saying it. I don't think anything here is well studied at all. It is not like we are all fishing in the dark but the organizational structures that determine the conditions in which software development and operations happen are not well understood. I found Herb Simon's writings and his concept of bounded rationality very lucid.

When we shift from "reliability" to "safety" we also need to shift from the individual to the system.

Curious what examples do you see there. I don't doubt the experience.

When I draw analogies of my past experiences to present situations, that does not mean that my past experiences are the best way to convince people of what is the right thing to do. I still need to do the hard work of pointing out what it is that is in the common interest and why eg deleting stuff and simplifying is good.

In such a discussion it won't help me to say people who disagree with me are generally just emotional, does it? Even if I may have encountered people with such emotional reactions.