FStar
TablaM
FStar | TablaM | |
---|---|---|
44 | 151 | |
2,624 | 183 | |
2.6% | 0.0% | |
9.9 | 0.0 | |
8 days ago | over 1 year ago | |
F* | Rust | |
Apache License 2.0 | Mozilla Public License 2.0 |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
FStar
- Lean4 helped Terence Tao discover a small bug in his recent paper
-
The Deep Link Equating Math Proofs and Computer Programs
I don't think something that specific exists. There are a very large number of formal methods tools, each with different specialties / domains.
For verification with proof assistants, [Software Foundations](https://softwarefoundations.cis.upenn.edu/) and [Concrete Semantics](http://concrete-semantics.org/) are both solid.
For verification via model checking, you can check out [Learn TLA+](https://learntla.com/), and the more theoretical [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf).
For more theory, check out [Formal Reasoning About Programs](http://adam.chlipala.net/frap/).
And for general projects look at [F*](https://www.fstar-lang.org/) and [Dafny](https://dafny.org/).
-
If You've Got Enough Money, It's All 'Lawful'
Don't get me wrong, there are times when Microsoft got it right the first time that was technically far superior to their competitors. Windows IOCP was theoretically capable of doing C10K as far back in 1994-95 when there wasn't any hardware support yet and UNIX world was bickering over how to do asynchronous I/O. Years later POSIX came up with select which was a shoddy little shit in comparison. Linux caved in finally only as recently as 2019 and implemented io_uring. Microsoft research has contributed some very interesting things to computer science like Z3 SAT solver and in collaboration with INRIA made languages like F* and Low* for formal specification and verification. But all this dwarfs in comparison to all the harm they did.
-
What are the current hot topics in type theory and static analysis?
Most of the proof assistants out there: Lean, Coq, Dafny, Isabelle, F*, Idris 2, and Agda. And the main concepts are dependent types, Homotopy Type Theory AKA HoTT, and Category Theory. Warning: HoTT and Category Theory are really dense, you're going to really need to research them.
-
Why is there no simple C-like functional programming language?
F* is a dependently typed language that can be transpiled to idiomatic C via the KReMLin compiler. It’s very ML-ish to write and you can leave out some proofs. It also has the benefit of being used to write a formally verified TLS implementation that’s in wide use throughout industry.
-
[Media] Genetic algorithm simulation - Smart rockets (code link in comments)
As I said, dependent types attempt to solve this problem. F* is a language where you can express complex logic as a type. The catch is, these types are checked by an SMT solver. If the solver can satisfy the type checking, then great, and you move on. If it can’t, you have no idea why, and either have to guess or manually write the proof anyway. Contrast this with Standard ML which has a proof of the soundness of its type system.
-
Prop v0.42 released! Don't panic! The answer is... support for dependent types :)
So kind of like F*? https://www.fstar-lang.org/
-
old languages compilers
F*
-
Pegasus spyware was used to hack reporters’ phones. I’m suing its creators; When you’re infected by Pegasus, spies effectively hold a clone of your phone – we’re fighting back.
Nevermind that academia has come up with far safer ways to do a few things but social norms & inertia prevent their wider adoption (well okay, it also has a barrier to entry in the education required to use it but I don't think someone with the knowledge to meaningfully contribute to an OS kernel can be considered uneducated nor unable to learn).
-
[Hobby] Amateur Generalist Programmer Seeking to Put Bugfixing Skills to Good Use
Maybe that's a little off topic here, but if you like fixing bugs, i suspect you might also enjoy showing that there are no bugs at all. Check out languages like F* https://www.fstar-lang.org/ It's a proof-oriented programming language. You can use it to write code that has no bugs at all. And you once you're done, can convert F* to C or other languages.
TablaM
-
YC's Latest Request for Startups
> Very curious if anyone knows how to pull this off.
I work in this space (small/mid-size).
The good news is that there are several "obvious" ways to pull this off because an ERP is the culmination of everything a company needs and does. So almost anything you can imagine on the software is part of it.
The bad news, and the reason everyone wants a solution, is that is truly a big space, and then you need E.V.E.R.Y.T.H.I.N.G.
---
My take is to start from the bottom, and build a much better version of Access/FoxPro (https://tablam.org).
Any medium/big ERP end being a specialized computing platform that needs:
- A programming language
- A database engine
- An orchestration engine
- ELT engine
- Auth
- UI/Report builders
And to be clear: NONE of the "programming language", "database engine", etc are a good fit today.
NONE.
This is the big thing, This is the reason (from a tech POW only) that most attempts fail.
This is the secret of why Cobol rule(d): Is all of this! but is too old! (also, this is why SQL still is best: Is almost this).
---
So, to pull this off, you need a team that knows what is "missing" from our current tools, makes a well-integrated package, and adds a "user-friendly" interface in a way that is palatable for the kind of user that uses excel (powerfully).
Is not that impossible. FoxPro was the best example of this kind of integrated solution.
P.D: This is my life's dream, to make this truth!
-
Ask HN: Looking for a project to volunteer on? (February 2024)
SEEKING VOLUNTEERS: TablaM relational language (https://tablam.org)
TablaM is an in-progress programming language to provide a more ergonomic experience for building data-oriented applications.
This means that where most languages are focused on low-level details or engineering at large, TablaM is tailored with some small & big design decisions to make it enjoyable to write applications for e-commerce, finance, ERPs, and similar.
Cool things:
- TablaM marry the array + relational models. It means we should get very little need for manual loops and all the ops are vectorized.
-
What if an SQL Statement Returned a Database?
Yeah, I worked on https://tablam.org and https://spacetimedb.com.
It becomes pretty clear that `order` is a significant property to make useful (and performant!) programs. "Duplicates" is also required to make usefull programs.
One nonobvious reason for this: You wanna report that a `customer` has a duplicated key `1`. If you CAN'T model `[(customer.id = 1), (customer.id = 1)]` then you can't report errors! And `erroneous` data is VITAL to make useful programs because then the only possibility is "perfect" data, and that is not possible!
Another reason is that we want to `count` duplicates, to see `duplicates`, and other NON-obvious at first: "What is a duplicate?". Get fun with floats, Unicode, combining case and non-case sensitive input... and is obvious that for useful programs IS REQUIRED to support bags in an extended version of the relational model.
And yet...
IS very important to remember about `set semantics` and try to adhere to it when makes sense. Your query planner will like it. You "valid" constraints like it. And `unique index` like it. And so on...
-
If you were dictator of the world what would you force programmers to write in?
Finally, for app development, I will "suggest" everyone use my lang https://tablam.org!
-
There are no strings on me
This is moe interesting than it looks, probably because the best part (IMHO) is about the type system, that is what enables the other ideas.
> In Julia, types are first-class and every value has a type
This is what I do from the start in https://tablam.org and only later found that is not common! Is so intuitive this way and simpler to check, by a lot. In fact, I waste so much time adapting type inference algorithms that are hard to translate because for some reason graphs are imposed on trees, types are second-class and live at a distance (and erased) and all is a mess this way.
The relational model already makes this so simple: `project / rename / extend` relational operators cover you.
From this other facilities become possible. Note how in `SQL` you don't have functions as first-class per se, but now try to imagine that a function is a table and suddenly, is much better!
-
Ask HN: Show me your half baked project
My relational lang (https://tablam.org) that I wish to be a Excel + Access replacement is still half-backed.
I move it slowly in my personal computer but not much in public. Maybe adding another person will help me on that!
-
Ask HN: Why did Visual Basic die?
> what is a good alternative to Access (or Fox, I add)
Nothing.
Access is(was) in fact a worse alternative to Fox:
- Much worse DB engine, and that is saying a lot (FoxPro db can and get corrupted. A typical functionality that was added to any fox codebase was a utility to fix it)
- MUCH MUCH worse programming language (VB) that is neither good as-is, much less as a data-programing language.
Fox/dbase is the only data-oriented language that was relatively popular and fit for the use-case.
This is by a mile the main point: Is a desert looking for languages that are made for business app/data oriented programing (and much harder looking for something not weird).
The main options: Fox/dBase/Informix(? not remember), kdb+, Cobol, SQL(when extended as store procedure lang with loops and that)
--
This point is big. Having a good form builder (that is already rare) is not enough to be a real contender for this space. You need a language where making queries is truly nice.
In short, you need a language that is `LINQ/Relational` as first-class end-to-end.
- If this lang needs an ORM: FAIL.
- If this lang needs to compose strings to make a query: FAIL.
- If exist "impedance mismatch" between data manipulation/queries and the rest of the lang: FAIL.
- It should also support super-advanced types like date, decimal, currency and ideally dimensional units. Ideally algebraic types as today.
- It should have a version of Rust `serve, Into/From` for easy conversion between data + formats.
- It should look "normal" like python/swift with `LINQ` queries.
This is the lang I trying to build: https://tablam.org
-
SQLite 3.43.0 Released
> I asked was about querying data without ever using a SQL language, like tapping directly into the data.
I agree (making https://tablam.org to try a fix & working on https://github.com/clockworklabs/SpacetimeDB in the SQL conformance).
Before I think SQL was bad. *Now I'm certain*. SQL is absurdly massive for things that could have collapse all the features 10x or more.
However, working in an RDBM now I also understand why is not desirable to make "raw" calls to the DB: The engine MUST mediate all the calls to make things works (from query optimization, execution, iteration, lock management, transaction management, etc).
Is incredible how much sophistication is in a simple `SELECT * FROM table`.
What I wish is to build a `Wasm-like` IR so that is what anybody target, and `SQL` is not the mediator.
-
How to start learning a systems language
In my case each lang I have learned (+12) I start coding a mini-ORM. I have done the same so many times, and that is a good way to learn from me. Also, I have to learn Rust building https://tablam.org.
-
Good languages for writing compilers in?
It sounds puzzling, I start learning Rust with https://tablam.org and probably was making my life harder trying to do "advanced" stuff when not have any idea of what I was doing.
What are some alternatives?
coq - Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
racket - The Racket repository
lean - Lean Theorem Prover
BQN - An APL-like programming language. Self-hosted!
dafny - Dafny is a verification-aware programming language
noria - Fast web applications through dynamic, partially-stateful dataflow
koka - Koka language compiler and interpreter
FunSQL.jl - Julia library for compositional construction of SQL queries
VisualFSharp - The F# compiler, F# core library, F# language service, and F# tooling integration for Visual Studio
wizer - The WebAssembly Pre-Initializer
stepmania - Advanced rhythm game for Windows, Linux and OS X. Designed for both home and arcade use.
wasmi - WebAssembly (Wasm) interpreter.