lean4 VS oil

Nice read! Rust has pushed, and will continue to push, the limits of practical, bare metal, memory safe languages. And it's interesting to think about what's next, maybe eventually there will be some form of practical theorem proving "for the masses". Lean 4 looks great and has potential, but it's still mostly a language for mathematicians. There has been some research on AI constructed proofs, which could be the best of both worlds because then the type checker can verify that the AI generated code/proof is indeed correct. Tools like Kani are also a step forward in program correctness.

Yeah, I believe they said intend for it to be used as a general purpose programming language. I used it to complete Advent of Code last year.

There are some really interesting features for general purpose programming in there. For example: you can code updates to arrays in a functional style (change a value, get a new array back), but if the refcount is 1, it updates in place. This works for inductive types and structures, too. So I was able to efficiently use C-style arrays (O(1) update/lookup) while writing functional code. (paper: https://arxiv.org/abs/1908.05647 )

Another interesting feature is that the "do" blocks include mutable variables and for loops (with continue / break / return), that gets compiled down to monad operations. (paper: https://dl.acm.org/doi/10.1145/3547640 )

And I'm impressed that you can add to the syntax of the language, in the same way that the language is implemented, and then use that syntax in the next line of code. (paper: https://lmcs.episciences.org/9362/pdf ). There is an example in the source repository that adds and then uses a JSX-like syntax. (https://github.com/leanprover/lean4/blob/master/tests/playgr... )

My latest inspiration to use code to a) replace my video editor, b) learn the basics of EDM production and c) understand a few topics in higher maths. This might sound very strange given there are specialised tools for these jobs. There's iMovie / Adobe Premier for video, there's GarageBand and FL studio for music and old good pen and pencil for math proofs. But these tools have three big limitations. First they have a lot of idiosyncratic learning, you have to spend quite some time getting used to these tools and my experience is that this time is quite upsetting. In contrast, you only have to learn to code one, maybe spend a few hours getting used to the syntax of another language. I'm not sure if that's true for most people but it was true for me using the tools mentioned above and wanted a place to discuss and see other people ideas and experiments. The second issue is that all these custom-made tools, are not composing easily. I can't search for all math proofs that used a single theorem. I can't create a plugin for iMovie and apply it to all my videos. I can't pick easily pick a rhythm from the internet and build upon for fun. There's also the issue of costs and version control, all tools I'm using today are open source and my work is stored in my repositories. This way I can create branches and test my ideas and I'm also confident that I can work in these projects in years.

Dafny and Whiley are two examples with explicit verification support. Idris and other dependently typed languages should all be rich enough to express the required predicate but might not necessarily be able to accept a reasonable implementation as proof. Isabelle, Lean, Coq, and other theorem provers definitely can express the capability but aren't going to churn out much in the way of executable programs; they're more useful to guide an implementation in a more practical functional language but then the proof is separated from the implementation, and you could also use tools like TLA+.

https://dafny.org/

https://whiley.org/

https://www.idris-lang.org/

https://isabelle.in.tum.de/

https://leanprover.github.io/

https://coq.inria.fr/

http://lamport.azurewebsites.net/tla/tla.html

Lean4 manages to pull off changing the parser on the fly at compile time. You can add new productions, add new syntax node types, and add new tokens. Then define macros or code to process the additional syntax. Here is a sample I found that adds a simple JSX-like syntax starting around line 93 and then uses it at line 169:

https://github.com/leanprover/lean4/blob/master/tests/playgr...

I believe most of the language is defined this way, although it is pre-compiled.

For more details see the lean4 metaprogramming book: https://github.com/arthurpaulino/lean4-metaprogramming-book

will prevent almost all of the "silent footguns".

YSH has strict:all and then a bunch of NEW features.

There's been good feedback recently, which has led to many concrete changes. So your experience can definitely influence the language! https://github.com/oilshell/oil/wiki/Where-To-Send-Feedback

Regarding writing tools/tests/benchmarks in bash+Python, vs. writing tools in your main language:

I think we might eventually concede that something Debian-like is the “standard development environment” (at least for server side stuff, i.e. not iOS apps)

In this case, bash+Python is a non-issue. It works extremely reliably. That’s actually why I use it! Everything else seems to break, or it’s really slow (node.js is a very common alternative).

- Microsoft conceded this back in ~2017, by building Linux into their kernel with WSL, and providing Ubuntu on top

Yes bash + Python is a disaster on Windows (I have scars from it), but Microsoft agrees that the right place to solve that is in Windows :-)

- Every CI system runs Debian/Ubuntu

- Every hosting provider runs Debian/Ubuntu

- Every online dev env like gitpod.io provides Debian/Ubuntu

This is somewhat related to remote dev envs: https://lobste.rs/s/ucirlx/lapdev_self_hosted_remote_dev

One vision for https://www.oilshell.org/ is that the CI environment is the dev environment is the hosting environment.

Everything is just an equal node in a distributed system. BUT it’s more git like, in that you explicitly sync and work “locally”, wherever that is. You don’t have the network chatter and flakiness of “the cloud”.

Oils has a very large set of monotonically increasing properties too - https://www.oilshell.org/release/0.21.0/quality.html

All that is bash+Python that is run on every commit, and it’s extremely good at catching bugs and perf regressions.

I’m skeptical that any project has that level of quality automation written in pure Rust or Zig. More likely it’s a bunch of cloud services with YAML.

Also a bunch of “hard-coded” toolchains that you can’t script with bespoke code. Like some shell commands in your package.json, which is just a worse way of writing a shell script.

Our quality process is all self-hosted, in the repo, and runs on both Github Actions and sourcehut - https://www.oilshell.org/release/0.21.0/pub/metrics.wwz/line...

bash and Python runs perfectly on Github Actions and sourcehut, with zero change. Containers also do.

(Although we need to unify the CI and release, because the release runs on 2 different real hardware machines, while CI is cloud only.)

Also, a main point Oils is that bash now has another highly compatible, spec-driven implementation – OSH. Having 2 independent implementations is something newer languages don’t have.

(copy of lobste.rs comment)

in your bashrc to enable it. I've used it for probably ~18 years now.

It also works with https://www.oilshell.org/ since we use GNU readline. Just 'set -o vi' in ~/.config/oils/oshrc

No other shell does that.

But I didn't know it was called MULTIOS until now. (I guess that's read "mult I/O's"? I have a hard time not reading it was multi-OS :) )

It seems a bit niche to be honest, but it's possible to support in Oils.

---

Oils also uses Unix domain sockets already for the headless shell protocol

https://github.com/oilshell/oil/wiki/Headless-Mode

We could do something like dgsh, but so far I haven't seen a lot of uptake / demand. Every time it's mentioned, somebody kinda wants it, and then it kinda peters out again ... still possible though.

I think flat files work fine for a lot of use cases, and once you add streaming, you also want monitoring, more control over backpressure/queue sizes, etc.

which works well. You don't have to clean when rebuilding variants. IMO this is 100% essential for writing C++ these days. You need a bunch of test binaries, and all tests should be run with ASAN and UBSAN.

---

I wrote a mini-bazel on top of Ninja with these features:

https://www.oilshell.org/blog/2022/10/garbage-collector.html...

So it's ~1700 lines, but for that you get the build macros like asdl_library() generating C++ and Python (the same as proto_library(), a schema language that generates code)

And it also correctly finds dependencies of code generators. So if you change a .py file that is imported by another .py file that is used to generated a C++ header, everything will work. That was one of the trickier bits, with Ninja implicit dependencies.

I also use the Bazel-target syntax like //core/process

This build file example mixes low level Ninja n.rule() and n.build() with high level r.cc_library() and so forth. I find this layering really does make it scale better for bigger projects

https://github.com/oilshell/oil/blob/master/asdl/NINJA_subgr...

Some more description - https://lobste.rs/s/qnb7xt/ninja_is_enough_build_system#c_tu...

This is sort of a category error...

re2c is a lexer generator, and YAML and Python are recursive/nested formats.

You can definitely use re2c to lex them, but it's not the whole solution.

I use it for everything possible in https://www.oilshell.org, and it's amazing. It really reduces the amount of fiddly C code you need to parse languages, and it drops in anywhere.

SEEKING VOLUNTEERS - https://www.oilshell.org/ - https://github.com/oilshell/oil/

I'm looking for people to help fill out the "standard library" for Oils/YSH. We're implementing a shell for Python and JavaScript programmers who avoid shell!

On the surface, this is writing some very simple functions in typed Python. But I've realized that the hardest parts are specifying, TESTING, and documenting what the functions do.

---

The most recent release announcement also asks for help - https://www.oilshell.org/blog/2024/01/release-0.19.0.html (long)

If you find all those details interesting (if maybe overwhelming), you might have a mind for language design, and could be a good person to help.

Surveying what Python and JavaScript do is very helpful, e.g. for the recent Str.replace() function, which is nontrivial (takes a regex or string, replacement template or string)

But there are also very simple methods to get started, like Dict.values() and List.indexOf(). Other people have already contributed code. Examples:

https://github.com/oilshell/oil/commit/58d847008427dba2e60fe...

https://github.com/oilshell/oil/commit/8f38ee36d01162593e935...

This can also be useful to tell if you'll have fun working on the project - https://github.com/oilshell/oil/wiki/Where-Contributors-Have...

More on #help-wanted on Zulip (requires login) - https://oilshell.zulipchat.com/#narrow/stream/417617-help-wa...

Please send a message on Github or Zulip! Or e-mail me andy at oilshell dot org.

This is true, but then the corrolary is that new PRs need to come with this higher and rigorous level of test coverage.

And then that becomes a bit of a barrier to contribution -- that's a harness

I often write entirely new test harnesses for features, e.g. for https://www.oilshell.org, many of them linked here . All of these run in the CI - https://www.oilshell.org/release/latest/quality.html

The good thing is that it definitely helps me accept PRs faster. Current contributors are good at this kind of exhaustive testing, but many PRs aren't