[caotic123]

You can always use let (in that our case def) to minimize the problem with inlining. I think functional programmers get used to big expressions because they do not inspect every symbol when they are reading, the context gives enough information! But you are correct, I couldn't make it better than its syntax/semantics because the implementation should be also very simple. And yes, PomPom is very simple compared to other proof assistants (we are not dealing only with functional programming but also dependent types).

[saithound]

I think you made good trade-offs regarding the syntax. Your language needs to be simple in the sense that it should not be complicated to parse unambiguously. But it also had to remain somewhat usable.

I think you made a good choice: it's easy to parse, and not all that difficult to read for the people who are likely to use it, after some minutes of deliberate practice.

Sure, it's quite symbol-heavy, and it's not as clean as, say, Agda or Idris. But (after a few minutes of practice) I find the difficulty entirely comparable to reading Coq.

Unsurprisingly, people who by their own admission never use functional, much less dependently typed, programming languages won't find it easy to read. But nothing you can do would make it easy to read for them, any more than you can make Jack Sprat easy to read for those who do not speak any English. To convey what it does, you'd have to write it in an entirely different language, and it would lose its very purpose in the process.

[caotic123]

Also, my current work/job is using Kind as a foundation, the purpose of this language is exactly what you have asked for, give a check on https://github.com/uwu-tech/Kind.

[jimsimmons]

Cool! No offence, I went on a rant hoping to start a discussion about FP. The fact that you have a dependently typed language in 1000 lines is an amazing feat. Don’t want to take anything away from that. I just wish the functional community took readability more seriously is all

[tluyben2]

Maybe it is because of when you are doing this all day, you really don't see this anymore? I can read j/k just fine, as well as Haskell, but I find many imperative languages noisy and basically ugly and unreadable. I like things terse and as much as I can on 1 screen so I don't have to scroll or remember things (when you get older, remembering wtf something was called again gets pretty annoying; very strict static typing and defining types precisely (aka a zipcode or telephone number are not strings!) together with terse functional constructs help a lot; the IDE will know everything so you can focus on implementation).

[devit]

Interesting!

Though it seems to share the problem of all current dependently typed languages of not supporting efficient implementation since everything has to be boxed and there are no linear types.

So you are forced to choose between something efficient but with no built-in dependent types like Rust or an horribly inefficient dynamically typed languages.

[erichocean]

> So you are forced to choose between something efficient but with no built-in dependent types like Rust or an horribly inefficient dynamically typed languages.

Or…use TLA+, which doesn't have types (but you instead define near-trivial type invariants that the model checker checks). This turns out to have a lot less ceremony, while producing extremely useful results quickly.

tl;dr TLA+ is a lot more practical if you care about bug-free software, and not even in the same universe in terms of difficulty as something like Coq. However, Coq can do fancy mathematics that TLA+ doesn't even try to do, so both should exist. (Neither are easy to learn, but TLA+ is much, much easier than Coq.)

I'm familiar with Coq, and reach for TLA+ and Alloy for practical programming. Coq is super-interesting, but ultimately not very practical for programming today. It's very nice for doing weird math stuff though. (You can't do any weird math stuff in TLA+.)

In the end, it kind of depends where you think you'll get the most bang for the buck with formal verification: can you confidently write correct code, if you get the design right? Or are you afraid that even with a flawless design/spec, you'll still screw up the code?

If it's the latter, Coq (and relatives) are what you want, though almost no-one uses the generated (read: provably correct) code. Expect to spend years on anything useful and produce at least one PhD, probably multiple, in the process. It's an absolutely enormous amount of work.

OTOH, if you're concerned that your proposed design might have issues, then TLA+ is many, many orders of magnitude more useful in practice, because it can help you produce a correct design with very little effort (days to weeks). TLA+ helps you find specification errors extremely easily, and the specs (once you get used to it) are easy to write.

Once the design/spec has been tested to work correctly in TLA+ (using a model checker), you still have to implement it (e.g. in Rust), but honestly, that's straightforward once the spec is correct and your mental model of the problem is solid. Highly recommended.

[amw-zero]

Have to jump in on a TLA+ comment, especially one about how it handles “types.” I say this all over the Internet - the way that TLA+ handles types is the absolute ideal from the programmer’s perspective - there is nothing special about them! No special syntax, semantics, nothing. It’s all the same language and logic, unlike most type systems which have a completely separate type language with subtly different semantics.

The problem is, that programmer simplicity pushes the complexity to the type checking. You can’t statically check TLA+ types, you have to model check them which is much more intensive.

Maybe there’s a happy medium.

[erichocean]

> You can’t statically check TLA+ types

I wish I could someday meet a programmer who's main problem, daily, is that their code won't type check. Otherwise, everything's great!

I like type checking, but not because the static type checker helps me write correct code. (When it does, the "bugs" it finds are trivial, at the same level as the syntax checker.)

I like type checking because it makes documentation easier, it makes writing code easier (code completion), because it means I can write fewer comments, etc. Not because of "correctness", and since that's the goal of something like TLA+, I haven't (yet) found myself wishing for it.

Especially with my experience using Coq, the way TLA+ handles types is a breath of fresh air. Simply lovely.

[amw-zero]

The trivial bugs that type systems are catching are in the most basic type systems that we know about. Types are not just what is present in Java, types are any proposition that can be made about a program before program execution. The propositions that a type system allows you to make is a design decision as well as an implementation challenge.

But if you look at something like F* or Idris, the types allow extremely rich propositions. I think you’re selling types short, even though they of course are not the answer to all problems.

[zozbot234]

> tl;dr TLA+ is a lot more practical if you care about bug-free software

TLA+ is not generally used for end-to-end checking of actual program code, unlike Coq. Usually you build a simplified "toy" model in TLA+ of some architecture of interest, then use model checking to try and refute some claimed properties of that model. If the model checker finds a refutation of some property, then yes, that's a verified bug in your toy model. If it fails to find one, that's not a proof of correctness other than in very special cases where a property can be checked finitely.

So yes, model checking is helpful in some cases, but it's not a generally useful tool. And there are ways to do the same things in general proof assistants, e.g. by interfacing them with external SMT tools. The TLA language in itself is also unproblematic, it simply adds modalities for time, state and non-determinism to ordinary logic, and there are well-known ways to convert ("embed") those features to a form that a proof assistant can work with.

[erichocean]

> TLA+ is not generally used for end-to-end checking of actual program code, unlike Coq.

To my knowledge, TLA+ is never used for checking program code. At least, I've never heard of anyone doing it.

> model checking is helpful in some cases, but it's not a generally useful tool

I strongly disagree. Spending time trying to "prove" in Coq an incorrect, flawed specification is an insane waste of time. A model checker can show you the problems in (literally) seconds.

Consider Raft, for instance, which was formally verified in Coq. You know what they did first? Write a TLA+ model, and then model check that until they got the design right. Trying to start in Coq (with an incorrect design) would not have been smart.

Model checkers are extremely useful tools.

----

Going further, the TLA+ spec of Raft is less that 500 lines.

The Coq proof of TLA+ is ~50,000 lines. It resulted in a verified implementation that to the best of my knowledge, no one uses in production.

It's a nice achievement, but in terms of usefulness? TLA+ has Coq beat by a country mile.

[zozbot234]

> Spending time trying to "prove" in Coq an incorrect, flawed specification is an insane waste of time. A model checker can show you the problems in (literally) seconds.

Sure, if there's anything a TLA+ model checker is good at it's searching for counterexamples. But in pretty much any case where such a search is computationally viable, it's also easy to set it up in a proof assistant. By and large, model checkers use the exact same toolset under the hood as the "sledgehammer" automated proof search in a proof assistant, such as SAT and SMT satisfiability solvers.

> It resulted in a verified implementation, that to the best of my knowledge, no one uses is production.

No one uses a TLA+ model directly in production either, because that's not what TLA+ is. The question only makes sense for a tool like Coq where one can work end-to-end with an actual implementation.

[nextos]

What do you think about Ada Spark?

[erichocean]

I don't have any direct experience with it.

[zozbot234]

AIUI, the integration of linear types (or substructural types in general) with dependent typing is still a matter of research. Even "simple" type system extensions like higher-kinded types come with a lot of added complexity.

There is also what's arguably a deeper obstacle to "efficient" implementation of dependent types because dependent typing does away with the phase separation between compile-time and run-time. We do have "program extraction" features in many DT languages to mitigate this, but they're still ad-hoc additions, there isn't yet a principled approach to the issue.

[AnthonBerg]

Idris 2 has quantitative dependent types. As far as I know quantitative types contain linear types. Are a superset. Idris typechecks 0 and 1 uses of types (and many).

It’s a great language.

https://idris2.readthedocs.io/en/latest/updates/updates.html...

The locus of the research that Idris’ linear types are based on might be Conor McBride’s paper I Got Plenty O’ Nuttin: https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.p...

It’s a beautiful paper.

There are other papers in between McBride’s paper and the implementation. They’re great papers too.

I find it telling that the Idris 2 source code for quantitative types in the Idris 2 compiler is beautifully readable and understandable. This is what tends to happen in Idris code. Clarity.