> On Nov 21, 2020, at 10:15 PM, Mario Carneiro <[email protected]> wrote: > > > > On Sat, Nov 21, 2020 at 8:42 PM David A. Wheeler <[email protected] > <mailto:[email protected]>> wrote: > Providing a Scheme-like interface is a reasonable approach. It’s easy to > implement & provides a lot of flexibility. The big problem is that MANY > people hate their syntax, e.g., “lots of irritating silly parentheses”. As > you know, I think it’d be *much* better if it supported neoteric syntax (at > least), so that you can use syntax like f(5) and {2 + 3}, as that eliminates > the main complaint about Lisps while retaining all their benefits. > > I'm inclined not to spend much time on this complaint. Better to spend some > time with it, get a sense for the way things are put together, and *then* > propose improvements. Alternate syntax is not out of the question but it > needs to fit within the other design constraints of the language. In > particular, MM1 is in many ways an MVP for a metamath based proof assistant, > enough to help me prove my big theorems and not much more. If this is to > become some big flagship product then I don't mind investing more to make it > convenient, but only after the more pressing problems are dealt with.
This is something I can easily do. I’ve implemented neoteric expressions in Scheme, Common Lisp, and Java. It turns out to be very short, *AND* they’re totally optional for use. That is, you can always say (foo bar bar) if you prefer it over foo(bar baz). > > If you’re picky about types, you could even trivially implement a > preprocessor to convert the Scheme-like language into Rust, and then compile > it into the result. Then, once you’re happy with something, you could > “freeze” into a faster Rust implementation. > > Indeed, I don't recommend going overboard with the metaprogramming because > the result isn't especially maintainable without static types. Complicated > tactics should be written as plugins, either in rust or dynamically linked > from another language. The main strength of the language is for micro-tactics > like when two branches of a proof are almost but not quite the same, and > simple pattern matching tactics like norm_num. Fair enough. > Java has garbage collection & semantics that are very familiar to many (e.g., > object orientation & references). > > Rust's approach to handling memory feels very similar to Java as an end user, > but it's quite different under the hood (the latter is obvious if you hear > the press, but the former might be more surprising). You almost never have to > explicitly drop things, and when you do it's usually because you need to > unlock a mutex or something like that that goes beyond regular memory > management. I would say Rust is more like Ada. Ada and C++ both don’t have built-in garbage collection, but instead use user-defined finalization to deallocate help memory. Ada is *unlike* C++, and more like Rust, in that Ada has strict static typing & generally tries to prevent errors at compile time. Ada doesn’t have borrow checking per se, but its SPARK variant does, and I know there’s a proposal to add borrow checking to Ada: https://www.adacore.com/uploads/techPapers/Safe-Dynamic-Memory-Management-in-Ada-and-SPARK.pdf > There are lots of verification-related technologies that don't have an LCF > style approach; SAT and SMT solvers, model checkers, and even some proof > languages like PVS and NuPRL come to mind. But I think MM1 is qualitatively > different from these examples, in that MM1 is a tool for producing a proof at > the end of the day, while the others are producing "correctness", with a > yea/nay answer at the end and nothing more. If that's all you have, you > really want to know that everything that goes into that yea/nay answer is > trustworthy, and that's just what our verifiers are doing. But with a proof > object, you can always just check it at your leisure. To be fair, some SMT solvers *do* have proof producing mechanisms (e.g., CVC4 and Z3). For comparisons, see: http://homepage.divms.uiowa.edu/~viswanathn/qual.pdf > ... > In summary, I don't think it's important to have a kernel given how many > backup plans we have, although any embedded verifier would be held to the > usual standards of correctness, but it can be done if we care to pursue this. Fair enough. I think we should make some efforts to detect problems “as early as reasonable”, but clearly we have a very strong final defense. > There might need to be some work so that the data structures are > easy-to-navigate & not fragile. I wonder if methods would be useful (e.g., > what appear to be “values” are really computed). I would hope a REPL could > query their state, and in some cases change them (though maybe only in > specific ways). > > In Rust, there is some focus placed on privacy as an abstraction mechanism. > You can have a struct with private fields, and provide public functions as > accessors to the data. This is especially important for anything around the > "kernel" like the Environment struct, since in a public API we probably want > to make it hard to misuse. Right now I think almost nothing in mm0-rs is > public, although a lot of things are pub(crate) (meaning accessible by other > code in the project but not from other modules). Making something public is > to some extent a stability promise; there are semver rules related to > changing the layout of a struct to add public fields and so on so each of > these things should be considered carefully once we have some user code that > wants to interface with it. Careful consideration is important, agreed. But I think we want to make sure that a lot of things are (eventually) accessible by a library call. If the library can be imported from (say) Python & JavaScript, and the library is eventually rich, then a whole lot of re-implementation does *not* need to happen. --- David A. Wheeler -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CB742D1D-72C0-46FD-9597-8E1148E29C99%40dwheeler.com.
