plainOldText

7 mesi fadiscuss

It's not strange at all.

The second story, and highly upvoted, on HN right now is: "AI will make formal verification go mainstream"[1].

[1] https://news.ycombinator.com/item?id=46294574

plainOldText

7 mesi fadiscuss

This Scott Wlaschin talk [1] is a good introduction to TLA+. And the slides [2].

[1] https://www.youtube.com/watch?v=qs_mmezrOWs

[2] https://speakerdeck.com/swlaschin/tla-plus-for-programmers

plainOldText

7 mesi fadiscuss

I guess it’s time to learn OCaml then.

It appears many of the proof assistants/verification systems can generate OCaml. Or perhaps ADA/Spark?

Regardless of how the software engineering discipline will change in the age of gen AI, we must aim to produce higher not lower quality software than whatever we have today, and formal verification will definitely help.

plainOldText

8 mesi fadiscuss

The main designer is Andreas Rumpf, but investigating the git commits of the new Nim reveals more people being involved. [1] Whether Andreas is a genius, I have no idea, but he has been doing compiler and language development for over 20 years [2] so he's probably extremely knowledgeable regardless.

[1] https://github.com/nim-lang/nimony/commits/master/

[2] https://en.wikipedia.org/wiki/Nim_(programming_language)

plainOldText

9 mesi fadiscuss

Reminder the creator of Wren wrote the awesome Crafting Interpreters book [0].

[0] https://craftinginterpreters.com/

plainOldText

9 mesi fadiscuss

The article allocates the last section to explaining why Rust is not a good fit (yet) so I wanted the title to cover that part of the conversation since I believe it is meaningful. It illustrates the tradeoffs in software engineering.

plainOldText

9 mesi fadiscuss

I’d be curious to know what the creators of SQLite would have to say about Zig.

Zig gives the programmer more control than Rust. I think this is one of the reasons why TigerBeetle is written in Zig.

plainOldText

9 mesi fadiscuss

It's interesting to observe how many people are undergoing an identity crisis due to the emergence of LLMs challenging the status quo.

What will our craft of programming turn into? So far programming has been quite fun and creative, but LLMs are undeniably changing the programmer's game. Will it still be as enjoyable? I don't know. But then, what else could we switch to which would allow us to be highly creative while still maintaining control?

Perhaps this is similar to how people felt during the industrial revolution.

plainOldText

9 mesi fadiscuss

You're absolutely right ((:

Now, seriously though, no tools is perfect, and I agree we should not trust it blindly, but leaving aside AI Agents, LLMs are very helpful in illuminating one's path, by consulting a large body of knowledge on demand, particularly when dealing with problems which might be new to you, but which have already been tackled one way or another by other people in the industry (provided they're in the training set of course).

Yes, there's always the risk of perpetuating existing slop. But that is the risk in any human endeavor. The majority of people mostly follow practices and knowledge established by the few. How many invent new things?

To be honest, I haven't yet used AI agents, I'm mostly just using LLMs as a dialogue partner to further my own understanding and to deepen my knowledge. I think we're all still trying to figure it out how to best use it.

plainOldText

9 mesi fadiscuss

A better term would be “Augmented Engineering” (AE).

You want something to inspire engineers to do their best work.

When you can expand your capabilities using the power of AI, then yeah, you can do your best work; hence augmented engineering.

But vibing? Not so much.

I guess AE could also stand for Advanced Engineering, after all the AI gives you the power to access and understand the latest in engineering knowledge, on demand, which you can then apply to your work.

plainOldText

9 mesi fadiscuss

Your example also gets evaluated at comptime. For more complex cases I wouldn't be able to tell you, I'm not the compiler :) For example, this get's checked:

  let ageFails = (200 + 2).Age
  Error: 202 can't be converted to Age

If it cannot statically prove it at comptime, it will crash at runtime during the type conversion operation, e.g.:

  import std/strutils

  stdout.write("What's your age: ")
  let age = stdin.readLine().parseInt().Age

Then, when you run it:

  $ nim r main.nim
  What's your age: 999
  Error: unhandled exception: value out of range: 999 notin 0 .. 200 [RangeDefect]

plainOldText

9 mesi fadiscuss

Nim was inspired by Ada & Modula, and has subranges [1]:

  type
    Age = range[0..200]

  let ageWorks = 200.Age
  let ageFails = 201.Age

Then at compile time:

  $ nim c main.nim
  Error: 201 can't be converted to Age

[1] https://nim-lang.org/docs/tut1.html#advanced-types-subranges

plainOldText

10 mesi fadiscuss

Nim is a statically typed language with a syntax resembling Python's. https://nim-lang.org/

Sometimes I'm questioning if it has the potential to become more popular in the future if AI becomes adept at translating Python projects to Nim.

plainOldText

10 mesi fadiscuss

Hmm, I guess this then makes sense if we regard the app as a latent space projecting user's data, so its views are awaiting to be activated.

Seen this way, the app is basically communicating to the user: Hey I have "Your Pictures", "Your Cases", etc. Click to find out.

But to me the "My ..." variation also makes sense. e.g. In Photos app on macOS you will see "My Albums", "My Projects", and although they can be renamed, I don't think I created them.

plainOldText

10 mesi fadiscuss

From the article:

> In summary:

> Use “your” when communicating to the user

> Use “my” when the user is communicating to us

I could see how this makes sense with dialogs.

But for UI elements? Should I name say a tab “My Pictures” and not “Your Pictures” because clicking on said tab I’m communicating to the system I want to see my pictures?

plainOldText

anno scorsodiscuss

Sorry, I wasn't clear. Yes, you can have pipelines in Flix, F#, OCaml, to me however placing the "subject" first feels more natural, as function signatures (not necessarily in pipelines) have a symmetry not encountered otherwise:

Subject First:

  Map.put(map, key, value)
  Map.get(map, key)
  Map.get(map, key, default)
  Map.del(map, key)

Subject Last:

  Map.put(key, value, map)
  Map.get(key, map)
  Map.get(key, default, map)
  Map.del(key, map)

plainOldText

anno scorsodiscuss

Heads up, the links to Paul Butcher's datalog posts are broken. The series can be found here now: https://paulbutcher.com/datalog1.html

plainOldText

anno scorsodiscuss

I think their DIDYOUKNOW.md file in the source code is worth showing in full, as it describes the language in a more compact form:

---

# Did You Know?

## Language

Did you know that:

- Flix offers a unique combination of features, including: algebraic data types and pattern matching, extensible records, type classes, higher-kinded types, polymorphic effects, and first-class Datalog constraints.

- Flix has no global state. Any state must be passed around explicitly.

- Flix is one language. There are no pragmas or compiler flags to enable or disable features.

- Flix supports type parameter elision. That is, polymorphic functions can be written without explicitly introducing their type parameters. For example, `def map(f: a -> b, l: List[a]): List[b]`.

- the Flix type and effect system can enforce that a function argument is pure.

- Flix supports effect polymorphism. For example, the `List.map` function is effect polymorphic: its purity depends on the purity of its function argument.

- in Flix every declaration is private by default.

- In Flix no execution happens before `main`. There is no global state nor any static field initializers.

- Flix supports full tail call elimination, i.e. tail calls do not grow the stack. Flix -- being on the JVM -- emulates tail calls until Project Loom arrives.

- Flix supports extensible records with row polymorphism.

- Flix supports string interpolation by default, e.g. "Hello ${name}". String interpolation uses the `ToString` type class.

- Flix supports the "pipeline" operator `|>` and the Flix standard library is designed around it.

- In Flix type variables are lowercase and types are uppercase.

- In Flix local variables and functions are lowercase whereas enum constructors are uppercase.

- Flix supports set and map literals `Set#{1, 2, 3}` and `Map#{1 => 2, 3 => 4}`.

- Flix supports monadic do-notation with the `let*` construct.

- Flix supports "program holes" written as either `???` or as `?name`.

- Flix supports infix function applications via backticks.

- Flix compiles to JVM bytecode and runs on the Java Virtual Machine.

- Flix supports channel and process-based concurrency, including the powerful `select` expression.

- Flix supports first-class Datalog constraints, i.e. Datalog program fragments are values that can be passed to and returned from functions, etc.

- Flix supports compile-time checked stratified negation.

- Flix supports partial application, i.e. a function can be called with fewer arguments that its declared formal parameters.

- the Flix type and effect system is powered by Hindley-Milner. The same core type system that is used by OCaml, Standard ML, and Haskell.

- the Flix type and effect system is sound, i.e. if a program type checks then a type error cannot occur at run-time. If an expression is pure then it cannot have a side-effect.

- the Flix type and effect system supports complete type inference, i.e. if a program is typeable then the type inference with find the typing.

- The Flix "Tips and Tricks"-section https://doc.flix.dev/tipstricks/ describes many useful smaller features of the language.

- Flix has a unique meta-programming feature that allows a higher-order functions to inspect the purity of its function argument(s).

- Flix names its floats and integers types after their sizes, e.g. `Float32`, `Float64`, `Int32` and `Int64`.

- Flix -- by design -- uses records for labelled arguments. Records are a natural part of the type system and works for top-level, local, and first-class functions.

- Flix -- by design -- has no implicit coercions, but provide several functions for explicit coercions.

- Flix -- by design -- disallows unused variables and shadowed variables since these are a frequent source of bugs.

- Flix -- by design -- disallows allow unused declarations. This prevents bit rot.

- Flix -- by design -- does not support unprincipled overloading. Instead, functions are given meaningful names, e.g. `Map.insert` and `Map.insertWithKey`.

- Flix -- by design -- does not support variadic functions. We believe it is better to pass an explicit array or list.

- Controversial: Flix defines division by zero to equal zero.

- Controversial: Flix defines String division as concatenation with the path separator. For example, `"Foo" / "Bar.txt" => "Foo\Bar.txt"` on Windows.

## Standard Library

Did you know that:

- Flix has an extensive standard library with more than 2,600 functions spanning more than 30,000 lines of code.

- the Flix Prelude, i.e. the functions which are imported by default, is kept minimal and contains less than 20 functions.

- most higher-order functions in the Flix standard library are effect polymorphic, i.e. they can be called with pure or impure functions.

- the Flix type and effect system enforces that equality and ordering functions must be pure.

- the Flix standard library uses records to avoid confusion when a function takes multiple arguments of the same type. For example, `String.contains` must be called as `String.contains(substr = "foo", "bar")`.

- the Flix `List` module offers more than 95 functions.

- the Flix `String` module offers more than 95 functions.

- the Flix `Foldable` module offers more than 30 functions.

- the Flix standard library follows the convention of "subject-last" to enable pipelining (`|>`).

## Ecosystem

Did you know that:

- Flix has an official Visual Studio Code extension.

- Flix has an official dark theme inspired by Monokai called "Flixify Dark".

- the Flix website (https://flix.dev/) lists the design principles behind Flix.

- Flix has an online playground available at https://play.flix.dev/

- Flix has online API documentation available at https://doc.flix.dev/

- the Flix VSCode extension uses the real Flix compiler.

- the Flix VSCode extension supports auto-complete, jump to definition, hover to show the type and effect of an expression, find all usages, and more.

- the Flix VSCode extension has built-in snippets for type class instances. Try `instance Eq [auto complete]`.

- the Flix VSCode extension supports semantic highlighting.

- the Flix VSCode extension has built-in "code hints" that suggests when lazy and/or parallel evaluation is enabled or inhibited by impurity.

- Flix has community build where Flix libraries can be included in the CI pipeline used to build the Flix compiler.

- Flix has a nascent build system and package manager based on GitHub releases. Today it is possible to build, package, and install Flix packages. Dependency management is in the works.

## Compiler

Did you know that:

- Flix -- by design -- has no compiler warnings, only compiler errors. Warnings can be ignored, but errors cannot be.

- the Flix compiler uses monomorphization hence primitive values are (almost) never boxed.

- the Flix compiler supports incremental and parallel compilation.

- the Flix compiler has more than 28 compiler phases.

- the Flix compiler contains more than 80,000 lines of code.

- the Flix compiler has more than 13,500 manually written unit tests.

- the performance of the Flix compiler is tracked at https://arewefast.flix.dev/

## Other

Did you know that:

- Flix is developed by programming language researchers at Aarhus University (Denmark) in collaboration with researchers at the University of Waterloo (Canada), and at Eberhard Karls University of Tübingen (Germany), and by a growing open source community.

- Several novel aspects of the Flix programming language has been described in the research literature, including its type and effect system and support for first-class Datalog constraints.

- Flix is funded by the Independent Research Fund Denmark, Amazon Research, DIREC, the Stibo Foundation, and the Concordium Foundation.

- more than 50 people have contributed to the Flix compiler.

- more than 2,000 pull requests have been merged into the Flix compiler.

plainOldText

anno scorsodiscuss

This language seems to be aiming high. Congrats!

Looking at their code however, I'm realizing one thing Elixir got "right", in my view, is the order of arguments in function calls.

For example, in Elixir to retrieve the value associated with a key in a map, you would write Map.get(map, key) or Map.get(map, key, default).

This feels so natural, particularly when you chain the operations using the pipe operator (|>):

  map
  |> Map.put(key, value)
  |> Map.get(key)

In Flix it seems one needs to write Map.get(x, map), Map.insert(x, y, map). I guess it follows in the footsteps of F#.

plainOldText

Submissions

Neural Computer: A New Machine Form Is Emerging

Performance Engineering: Algorithms for Modern Hardware

OpenBSD Jumpstart

Optimizable Code (2013)

Why Is SQLite Coded In C

Erlang ARM32 JIT is born

Phoenix Creator Argues Elixir Is AIs Best Language

comments