September 2022:
This has spread to a far wider audience than I had anticipated - probably my fault for using a title that is in hindsight catnip for link aggregators. I wrote this back in 2021 just as a bunch of personal thoughts of my experiences using Rust over the years (not always well thought through), and don't intend on trying to push them further, outside of personal experiments and projects.
Managing a living language is challenging and difficult work, and I am grateful for all the hard work that the Rust community and contributors put in given the difficult constraints they work within. Many of the things I listed below are not new, and there's been plenty of difficult discussions about many of them over the years, and some are being worked on or postponed, or rejected for various good reasons. For more thoughts, please see my comment below.
:- module(core, | |
[ % Operational semantics | |
eval/2, % +Expr, -VExpr | |
quote/2, % +VExpr, -Expr | |
normalise/2, % +Term, -Term | |
eval/3, % +Env, +Expr, -VExpr | |
quote/3, % +Len, +VExpr, -Expr | |
normalise/3, % +Env, +Term, -Term |
AUTOMATH/De Bruijn Notation-inspired, but extended with dependent records.
This is a more succinct syntax than the previous gist,
this time using in
and out
in place of param
and record
,
and making introductions and eliminations more succinct.
Further messing around on top of some ideas in the previous gist.
AUTOMATH/De Bruijn Notation-inspired, but extended with dependent records.
term, type ::=\
Playing around with a uniform notation for binders (eg. Π, Σ, λ, let). This is probably not the greatest language to program in directly, but I think it's fun to see if a more consistent syntax can help to expose some of the differences between dependent functions, dependent pairs, and let expressions...
I always get confused about terms, types, expressions, etc. in full spectrum dependent types… so toying around with these :sparkles: very informal :sparkles: Venn diagram thingies.
Note: Don't take this super seriously or authoritatively, it's more me trying to figure things out, and I'm very sloppy at this stuff!
/- | |
Playing with monoids in Lean 4 | |
``` | |
$ lean -v | |
Lean (version 4.0.0-nightly-2021-02-28, commit 6a6f68f6ccc8, Release) | |
``` | |
-/ | |
namespace Monoids |
/- | |
A proof of the correctness of an arithmetic expression compiler in Lean 4. | |
Ported from [expcompile.v], which is part of Derek Dreyer and Gert Smolka's | |
[course material]. | |
[expcompile.v]: https://www.ps.uni-saarland.de/courses/sem-ws17/expcompile.v | |
[course material]: https://courses.ps.uni-saarland.de/sem_ws1718/3/Resources | |
-/ |