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.
No it's already explicitly stated that translation to lean is a second step that happens after NL proof is done. That's why some of 400 paper dump is without lean proofs.
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.
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.
Maybe better performance can be achieved with specialized models. There are some that were able to solve mathematical olympiad problems, e.g. AlphaProof.
> 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".
Yes, but then those languages usually implement only unchecked exception, as propagating error types up the call tree is seen as annoying. And then, because there are good reasons you may want to have typed error values (instead of just "any"), there is now pressure to use result types (aka. "expected", "maybe") instead - turning your return type Foo into Result<Foo, ErrorType>.
And all that it does is making you spell out the entire exception handling mechanism explicitly in your code - not just propagating the types up the call tree, but also making every function explicitly wrapping, unwrapping and branching on Result types. The latter is so annoying that people invent new syntax to hide it - like tacking ? at the end of the function, or whatever.
This becomes even worse than checked exception, but it's apparently what you're supposed to be doing these days, so ¯\_(ツ)_/¯.
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.
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.
reply