siknad

I wonder how are they sure the proof is correct before making a Lean translation. How is the work loop organised to force LLMs to reach a valid solution. I thought the ability to make it possible was the main advantage of using Lean.

OpenAI having NL proofs earlier than Lean ones would require trust in the proof without ability to check it automatically. Perhaps Lean proofs are published later because it is considered a less important implementation detail or because there is a cleanup step that takes time.

Compile time evaluation is used in Lean all the time for metaprogramming (e.g. proof automation). Any `IO` can be run there (which allows running external solvers, reading a dataset from disk etc).

Perhaps access to IO in metaprograms could be restricted, but it would require substantial changes to the language and it is probably not a priority of the developers right now.

Lean is intended by its authors to be also used as a general-purpose programming language. Lean stdlib contains an HTTP server for example.

IMO the biggest problems are the lack of documentation, instability and poor ecosystem. There are user libraries for some programming tasks (e.g. HTTP router, graphics API bindings) but they are mostly proofs of concept and not actively developed or maintained.

Alternatively, the Writer can be replaced with "IO", then the messages would be printed during the processing.

The computation code becomes effectful, but the effects are visible in types and are limited by them, and effects can be implemented both with pure and impure code (e.g. using another effect).

The effect can also be abstract, making the processing code kinda pure.

In a language with unrestricted side effects you can do the same by passing a Writer object to the function. In pure languages the difference is that the object can't be changed observably. So instead its operations return a new one. Conceptually IO is the same with the object being "world", so computation of type "IO Int" is "World -> (World, Int)". Obviously, the actual IO type is opaque to prevent non-linear use of the world (or you can make the world cloneable). In an impure language you can also perform side-effects, it is similar to having a global singleton effect. A pure language doesn't have that, and requires explicit passing.

New mainstream languages are rarer than new better (in some way that can be favorable) languages.

Perhaps together with Agda (compiles to Haskell, has FFI to it, is more higher-level), some not-pure ML, and maybe Rust or ATS?

Maybe better performance can be achieved with specialized models. There are some that were able to solve mathematical olympiad problems, e.g. AlphaProof.

We could make explicit effect (context, error) declarations for public functions and inferred for private functions. Explicit enumeration of possible exceptions is required for stable APIs anyway.

> against the principles behind statically-typed languages, which all hate implicit things

But many statically typed languages allow throwing exceptions of any type. Contexts can be similar: "try catch" becomes "with value", "throw" becomes "get".

VS Code support for Common Lisp is lacking. Alive extension is relatively recent and is a solo effort and thus has significant bugs and is not as feature packed as Vim/Emacs alternatives. For example, it doesn't provide structural editing. It's interaction with sbcl cache seemingly broke my project a few times.

> Regarding pattern-matching and enum types, I can see why a C++ programmer is impressed with such constructs, but it's really underwhelming for an OCaml/Haskell programmer.

What's underwhelming about Rust's enums and pattern matching? Lacking indexed types/GADTs?

> I even wonder if it's necessarily a better choice than modern C++ for someone starting a new project.

The same enums, matching and other language features that aren't related to safety and yet allow the developer to write less boilerplate, alleviate the need to remember implementation details of the code used. And as someone said here, safety is not only about security vulnerabilities.

Not once I had problems with the borrow checker. Maybe it depends on the domain, requirements or project size. While I haven't finished any game in Rust, I am writing one (as a hobby/learning) and I try to avoid unnecessary and noticeable performance hits. Though I am working under the assumption that some runtime checks that are present in safe Rust and not in C++ are a net positive due to easier debugging. I'm not convinced that "unsafe" code and asm are necessary in modern gamedev.

Bevy has support for dynamically described components and systems. Their main use-case is scripting language support. Can't agree that they insist on single language approach.

> Lack of access to the C libraries.

Isn't CFFI enough for that?

> There is nothing compelling about the language to people who aren't already Lisp people.

CL is expression based (like Rust, unlike other mainstream languages I've seen), has a concise macro system (more convenient than Rust's imo), has a GC (simpler to use than languages with manual memory management or RC-only), has a better developed ecosystem then some new languages (ex. automatic ffi generation; while buggy, tremendously helpful compared to writing bindings manually). And it's not pure as in Haskell. And it has type annotations that may be checked at runtime or improve performance. An implementation like SICL could make it viable to use it as a scripting language.

Any similar modern languages with better tooling/ecosystem? Perhaps Julia, haven't seen it yet.