search

magmide / magmide

A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
811 stars 13 forks source link

Basil - same syntax, same computational power in compile-time as in runtime #5

Closed dumblob closed 3 years ago

dumblob commented 3 years ago

I wonder whether you could make some use of the (IMHO mind-blowing in a sense) language Basil (some cool features) as it offers "compile-time first" approach to writing apps because its syntax is the very same thing in compile-time as in runtime with zero differences.

Basil is thus not a "new level" of metaprogramming, but the "highest possible level" of metaprogramming. This has serious implications for just about anything and especially safety - because my incentive is to leverage the full power to create safety primitives tailorable to every imaginable use case (pretty much how you describe in your readme the "level of safety" required when importing libs or reusing existing code on new places).

Thoughts?

glyn commented 3 years ago

I didn't find the links above very helpful. This is more informative: https://github.com/nmacadam/basil. The language doesn't seem to offer any support for proof of correctness.

dumblob commented 3 years ago

@glyn the link you provided is a different language. The Basil I linked should allow for arbitrary proofs of correctness - because the compile-time computational capability is turing complete (but not in a sense as C++ templates are turing complete but with seamless full access to arbitrary part of the language).

glyn commented 3 years ago

@dumblob What threw me was your second link (some cool features) which points at a Twitter account, rather than any list of cool features of Basil.

dumblob commented 3 years ago

If you look closely at the content on the Twitter account, there are some announcements about "cool" features to get a very general feeling where the ecosystem is heading.

But all examples and implementation of the language is of course in its repository (first link "Basil").

blainehansen commented 3 years ago

@dumblob I think the main thing you're excited about in the basil design is homoiconicity? https://en.wikipedia.org/wiki/Homoiconicity

It's true that any self-hosting metaprogrammable language could possibly be used to build a custom type system or embedded dsl, which could be dependently typed or allow proving. Most don't though :)

I think I agree with @glyn that it was difficult to pull out lessons from those two links. Perhaps the readme could say a bit more about how the language actually works? I haven't had a lot of time to look at it, but the examples didn't really help me understand what's unique about it.

dumblob commented 3 years ago

@dumblob I think the main thing you're excited about in the basil design is homoiconicity? https://en.wikipedia.org/wiki/Homoiconicity

Not at all. I don't care about homoiconicity (it's only visually appealing, but not very useful in practice).

It's true that any self-hosting metaprogrammable language could possibly be used to build a custom type system or embedded dsl, which could be dependently typed or allow proving. Most don't though :)

IMHO Basil is different in that it kind of depends on you doing correctness checking (actually kind of dependent types checking and even more) unlike other metaprogramming languages. It's because of the "compile-time first" semantics (see below).

Btw. which other self-hosting fully metaprogrammable languages do you have in mind? With "fully" I mean the strict distinction between compile-time and runtime along with turing completeness in both (note, that self-hosting is part of what I sometimes refer to as "seamlessness" - i.e. if these properties are being achieved through transpilation to another language, it doesn't count here :wink:). I know only 2 or 4 such languages: Basil, Unseemly, maybe Passerine (still in development, so it's too early to judge) and maybe XL (it seems the compile-time and runtime distinction ceased with the newest releases because of complexity). And all of them get close to "something like dependent type checking" with "occasional proofs in various forms - e.g. explicit exhaustive search".

I think I agree with @glyn that it was difficult to pull out lessons from those two links. Perhaps the readme could say a bit more about how the language actually works? I haven't had a lot of time to look at it, but the examples didn't really help me understand what's unique about it.

Unique is the "compile-time first" approach - every single part of the graph gets evaluated in compile time unless impossible (e.g. due to dependency on some inherently runtime input). There are still some open questions in corner cases (especially regarding typing), so feel free to follow the development of Basil.

blainehansen commented 3 years ago

Ah I see, so it's a language that fully reduces any known values at compile time. I think there could be cool stuff there! I'll read some of these links when I get a chance :)