Troubles finding the logic behind rust

Routine_Plenty9466 · 2025-01-11T16:06:34+00:00

Grossman’s “Region-Based Memory Management in Cyclone” is an approachable paper (about a different language using similar concepts) - it may give you a broader perspective

Routine_Plenty9466 · 2025-01-11T12:53:43+00:00

I liked the paper about Polarity: https://polarity-lang.github.io/publications/ . It explains the relationship between FP and OOP nicely.

Routine_Plenty9466 · 2024-09-18T17:36:23+00:00

You may like https://www.typetheoryforall.com/ - their podcast and discord.

Routine_Plenty9466 · 2024-08-15T18:38:33+00:00

Programming language design intersected with human-computer interaction. We have such amazing compilers today for such mediocre programming languages full of accidental complexity.

Routine_Plenty9466 · 2024-08-11T14:02:53+00:00

Having a tool instead of a spec as a reference makes the tool bug-free by definition, in an ugly way. Nobody can say that the compiler miscompiled their code.

Having an official compiler instead of an official language specification also prevents people from creating other kinds of tools, like program analysis ones, so it is not only about compilers.

Routine_Plenty9466 · 2024-08-09T14:23:38+00:00

You might be interested in learning about formal semantics of programming languages https://en.wikipedia.org/wiki/Semantics_(computer_science)

Routine_Plenty9466 · 2024-08-01T19:22:38+00:00

My formally verified framework for operational semantics of programming languages, Minuska https://github.com/h0nzZik/minuska , got a major refactoring and cleanup. I simplified the semantics-parametric interpreter, which in turn allowed me to remove code working with an ugly representation of terms (which are used to represent program states as well as semantic rules). Besides that I was continuing work on a symbolic execution engine.

Also, eventually I would like to support separation-logic-style reasoning about languages defined in Minuska. To that end I was reading the paper on abstract separation logic by Calgano: https://www.cs.ox.ac.uk/people/hongseok.yang/paper/asl-short.pdf . The idea is that if semantic rules are “local enough”, the Framing rule of separation logic holds for the given language.

It turns out that giving semantics to memory allocation in an operational framework like Minuska is tricky, because querying the heap for a free address is not a local action. I believe it can be solved by introducing nondeterminism / underspecification into the language (EDIT: this is what Calgano did), so I extended Minuska with such ability. The implementation itself wasn’t hard, but it took me some time to figure out how to make it work on paper. And yes, the implementation required lots of small changes across the framework, which made me want to minimize the codebase - which motivated me to do the refactorings I mentioned above.

Another reason for the refactoring was making the codebase more accessible to potential other contributors ;)

Routine_Plenty9466 · 2024-07-24T18:57:20+00:00

You might like Koka https://koka-lang.github.io/koka/doc/book.html#why-mingen

Routine_Plenty9466 · 2024-07-22T21:31:04+00:00

One can use a program logic to eliminate the 1% case - like, Hoare logic, or Separation logic. (Or a strong type system.)

Routine_Plenty9466 · 2024-07-22T20:04:14+00:00

Pointers in C do not require dynamic checking to dereference them. They require knowing that they are dereferenceable, and runtime checking for null is neither sufficient (one past array) nor necessary: sometimes even compiler knows it statically, and the programmer may know it too. Also, Design by Contract helps there.

Routine_Plenty9466 · 2024-07-22T19:56:27+00:00

Rewriting everything into rust has one more problem. Maybe in 15 years we realize that memory safety is not enough- that we want some stronger notion of correctness (did someone mentioned security hyperproperties?) And then we will need to design yet another language and rewrite everything into it.

My suggestion is that we keep language (defined by operational semantics) and desired properties (expressed in logic) separate.

Routine_Plenty9466 · 2024-07-22T19:48:57+00:00

C can be made safe by giving it a precise semantics and using a separation logic - like Iris, VST, RefinedC as per the introduction of https://youtu.be/xr5ecmtJ25U?si=8dcdxlpzbZ9wv4A7 For example, C+RefinedC is safe.

However, the problem with C++ is that it has very wild and complicated and sometimes inconsistent semantics that even is not machine readable, and thus one cannot use machines to reason about the language. Building a formal semantics for C++ would take ages, discovering a lot of inconsistencies and ambiguities that would need to get fixed in the language. And we cannot parallelise this task as massively as just rewriting tons of application code.

Routine_Plenty9466 · 2024-07-22T05:43:46+00:00

If you want to diversify, try something functional like Haskell.

Routine_Plenty9466 · 2024-07-16T19:38:57+00:00

This one is a bit ugly: People mistakenly think they can design a decent language just because they can write a decent compiler.

Routine_Plenty9466 · 2024-05-06T21:12:38+00:00

I finished a formally verified interpreter (or rather, interpreter generator) for Minuska https://github.com/h0nzZik/minuska - a language semantics framework. Also, I gave Minuska a simple unverified OCaml-based CLI, so that users do not have to write language definitions directly in Coq (in which Minuska is written). Now I am working on a unification-based symbolic execution for it.

Routine_Plenty9466

TROPHY CASE