I like a lot of the idea behind such theorem provers, however, I always have issues with them producing compatible code with other languages.
This happened to me with idris and many others, I took some time to learn the basics, wrote some examples and then FFI was a joke or code generators for JavaScript absolutely useless.
Apart from prioritizing FFI (like Java/Scala, Erlang/Elixir), the other two easy ways to bootstrap an integration of a new obscure or relatively new programming language is to focus on RPC (ffi through network) or file input-output (parse and produce well known file formats to integrate with other tools at Bash level).
I find it very surprising that nobody tried to make something like gRPC as an interop story for a new language, with an easy way to write impure "extensions" in other languages and let your pure/formal/dependently typed language implement the rest purely through immutable message passing over gRPC boundary. Want file i/o? Implement gRPC endpoint in Go, and let your language send read/write messages to it without having to deal with antiquated and memory unsafe Posix layer.
“The current interface was designed for internal use in Lean and should be considered unstable. It will be refined and extended in the future.“
My point is that in order to use these problem provers you really gotta be sure you need them, otherwise interaction with an external ecosystem might be a dep/compilation nightmare or bridge over tcp just to use libraries.
If you look at their comment history it's quite clear that's what they are.
What's the HN stance on AI bots? To me it just seems rude - this is a space for people to discuss topics that interest them & AI contributions just add noise.
Serious question: why won’t JUST use SELinux on generated scripts?
It will have access to the original runtimes and ecosystems and it can’t be tampered, it’s well tested, no amount of forks and tricky indirections to bypass syscalls.
Such runtimes come with a bill of technical debt, no support, specific documentation and lack of support for ecosystem and features. And let’s hope in two years isn’t abandoned.
Same could be applied for docker or nix Linux, or isolated containers, etc… the level of security should be good enough for LLMs, not even secure against human (specialist hackers) directed threads
It was better because it had no silent errors, like 1+”1”. Far from perfect, the fact it raised exceptions and enforced the philosophy of “don’t ask for permission but forgiveness” makes the difference.
IMHO It’s irrelevant it has a slightly better typesystem and runtime but that’s totally irrelevant nowadays.
With AI doing mostly everything we should forget these past riddles. Now we all should be looking towards fail-safe systems, formal verification and domain modeling.
Conflating types in binary operations hasn't been an issue for me since I started using TS in 2016. Even before that, it was just the result of domain modeling done badly, and I think software engineers got burned enough for using dynamic type systems at scale... but that's a discussion to be had 10 years ago. We all moved on from that, or at least I hope we did.
> Now we all should be looking towards fail-safe systems, formal verification and domain modeling.
We were looking forward to these things since the term distributed computing has been coined, haven't we? Building fail-safe systems has always been the goal since long-running processes were a thing.
Despite any "past riddles", the more expressive the type system the better the domain modeling experience, and I'd guess formal methods would benefit immensely from a good type system. Is there any formal language that is usable as general-purpose programming language I don't know of? I only ever see formal methods used for the verification of distributed algorithms or permission logic, on the theorem proving side of things, but I have yet to see a single application written only in something like Lean[0] or LiquidHaskell[1]...
I think the only people who burnt of the discussion were people who is terminally online. But in the industry, there is people in any paradigm with any previous development times you can remember of.
> Is there any formal language that is usable as general-purpose programming language I don't know of?
That’s sort of my point, the closest thing to a rich type system yet pragmatic enough is to me F# and it’s still falls short as formal verification and ecosystem integration.
I think eventually, we should invest into this direction so LLM production can be trusted, or even ideally, producing or helping with the specific specifications of models. This is yet to be done.
I don’t want to make a prophecy, but the day, ergonomics and verification meet in an LLM automated framework, this new development environment should take over everything previous.
> With AI doing mostly everything we should forget these past riddles.
How I finally was able to make a large Rust project without having to sacrifice my free time to really fully understand Rust. I have read through the Rust book several times but I never have time to fully “practice” Rust, I was able to say screw it and built my own Rust software using Claude Code.
compressing the kernel loads it faster on RAM even if it still has to execute the un compressing operation. Why?
Load from disk to RAM is a larger bottleneck than CPU uncompressing.
Same is applied to algorithms, always find the largest bottleneck in your dependent executions and apply changes there as the rest of the pipeline waits for it.
Often picking the right algorithm “solves it” but it may be something else, like waiting for IO or coordinating across actors (mutex if concurrency is done as it used to).
That’s also part of the counterintuitive take that more concurrency brings more overhead and not necessarily faster execution speeds (topic largely discussed a few years ago with async concurrency and immutable structures).
No one thought juniors would be more benefited than seniors. St some people some said everything would be automatic and seniors would disappear altogether with programming itself.
But that was just said by crappy influencers whose opinion doesn’t matter as they are impressed by examples result of overfitting
This might depend on where you live and the kind of business… last time I made an Unmeldung online I needed to call after a week waiting and they literally told me that in person would be solved the same day. And it was.
Today I wasted 1 hour looking in how to use or where to find "Deep Research”.
I could not. I have the business workplace standard, which contains the Gemini advance, not sure whether I need a VPN, pay a separate AI product, or even pay a higher workplace tier or what the heck is going on at all.
There are so many confusing products interrelated and lack of focus everywhere that I really do not know anymore whether it is worth as an AI provider.
if it would make whole market research on products and companies I would gladly pay for it... but a bit unsure from Europe where it seems to be everything restricted due political boundaries.
Thanks for the offering, seriously, it is an important investment/cost I wasn't sure it would be worth right now. (If you wish to I added some contact information, for an easier chat, in my HN profile; just for the following day).
Here is a realistic case I would have used
Short prompt: "research the market of the SysML products and industry cap, key actors, opportunities and advantages"
Expanded prompt:
“Conduct a detailed market analysis of SysML (Systems Modeling Language) products and services, focusing on the following aspects:
1. Industry Overview:
• Current market size and growth trends for SysML-related products and services.
• Global market cap or valuation of the SysML industry or similar system engineering software.
2. Key Players:
• Identify major companies and organizations offering SysML tools, including established leaders and emerging competitors.
• Provide a brief description of each key player’s products, innovations, and market share.
3. Product Offerings:
• Highlight the range of SysML-based products available (e.g., modeling software, integration tools, training services).
• Compare features, target industries, and pricing strategies.
4. Market Opportunities:
• Explore new or underserved industries where SysML adoption could grow (e.g., aerospace, automotive, healthcare).
• Identify gaps in current product offerings that represent potential areas for innovation or competitive advantage.
5. Competitive Advantages:
• Analyze what makes SysML valuable to companies (e.g., improving system complexity management, ensuring design consistency).
• Evaluate how SysML tools offer a competitive advantage compared to alternative solutions like UML or other system modeling methods.
6. Challenges and Risks:
• Discuss potential challenges such as market saturation, training requirements, or competing technologies.
• Highlight external factors that could affect market growth, such as regulations or advances in adjacent industries.
Provide sources where relevant, including reports, studies, or insights from industry experts.”
Let me know what you think, will ya? I'm curious as to how you'd evaluate the quality of that report.
Also note the follow-up prompt I gave it. This thing needs as much detail as you can give it, and small changes to your prompt can hugely influence the end result.
Wow, thank you so much, that was 11 pages full pages. I will be a bit critical with it hoping my review helps you as well, since to me, it was very friendly and useful your offer (also I wonder if you can still do 99 more reserachs like this one during the month or this amounts already to many of such research in total).
Superficially:
- Awesome how fast is available and all sources linked to explain each claim
- To export that to a proper doc with footnotes and proper formatting it's already something to be worked by openAI
- it looks like the perfect way to create a gut feeling and a sense of what is going on
Content:
- Wrong studies: It mixed SysML (a particular visual language for which it was specifically requested) with MBSE (the family of tools) which is exactly not the same as the desired study was particular for SysML.
- Quality of data: Most of the data comes from public articles and studies made by others, all the time about MBSE, not SysML, and just quotes their numbers, it does not do its own estimates looking for the benefits of such products on each company and estimating a projection (that would be an actual research, and an AI should be capable of tirelessly do that or even biasedly look for the right pieces if information). For example it was a report on diet, a report like that should avoid debunk articles, bro's blogs, etc.
- Inconsistent scales: at some comparison table, it mentioned at the foot that it will display pricing with such schema:(Pricing: $ = low, $$$$ = high) however it made that in a single row. Why? the source for that field made that as well in its source, but none of the other fields repeated this system to value or adapt results.
- Only googleable data: companies reports or private databases here are key for a high quality report. Sometimes this is not always possible for an AI or a crawler but here am I evaluating the outcome (use case): a market analisis for strategic purposes.
- Quality of the report: Many things mentioned like services around the products are also highly valuable... would be useful to remark case by case the business model of each company and how much is in the product and how much is in the related service (using a pie chats or whatever) and showing particular case studies to remark the market trend, from which model is coming from (product) and where it is going to (services and SaaS).
I could continue longer with many other things and such errors but it is quite long.
Conclusion:
It is very useful, particularly to grasp a general, yet detailed, idea on what is going on, on a market. However it is only as valid as a remix of previous things, not an actual market research for an actual strategy. Many sources, elements, landscape of which companies and products related are there are totally useful, perhaps 30%-40% of the total work and it gives a clear structure where to go from here.
Probably it may improve the more interactive that the tool is, for example asking to correct some sections or improve in specifically suggested ways by the user. Basically the user needs to bring expertise, reasoning from the field and critical thinking (things machines will be lacking in any foreseeable future).
Why am I so critic? Remember, map is not the territory, particularly in strategic terms. And it is also a problem that many professionals do also these kind of failures: uncritically copying data from other's reports without verifying critically any of it which leads to very specific kinds of strategic errors.
It will become more useful as it becomes specialized in the kind of reports, and judges critically (which does not) and if it can be adapted to work on a private repo or preselected amounts of sources, or even prescripted agent behaves for the sort of report.
Verdict:
I would purchase it, not to solve the problem or resell it, but as a way to get started and accelerate the process. It already does what an internship student would do, or a mediocre professional: revamp preexisting mashups to get a general, but detailed, feeling but no more insights or research than what it is already well known (googling after all).
It has a great future as it would be great if such level of non creative work is automated away as their value often is marginal and uncritically propagates previous beliefs and biases (and if there is a centralized tool, that can be tuned to avoid well known issues)
> It is very useful, particularly to grasp a general, yet detailed, idea on what is going on, on a market. However it is only as valid as a remix of previous things, not an actual market research for an actual strategy. Many sources, elements, landscape of which companies and products related are there are totally useful, perhaps 30%-40% of the total work and it gives a clear structure where to go from here.
> Probably it may improve the more interactive that the tool is, for example asking to correct some sections or improve in specifically suggested ways by the user. Basically the user needs to bring expertise, reasoning from the field and critical thinking (things machines will be lacking in any foreseeable future).
Yeah, that's just the thing. With what you know, you can iterate on the results it gives you. It's very sensitive to how your prompt is written and structured, so some fine tuning, user-provided context, and user expertise, it'll dial-in on any subject very well. It's not top-expert-level yet -- at least not on its own -- but it's close, and it's miles better than asking o1-Pro (or Deepseek r1) for a detailed report.
Just post your prompt here and I'll give you a link to the response. Deep research requires pretty detailed prompts in order to generate high-quality reports.
I'm usually in Croatia but am right now in Greece. My account ($200 Pro account) works the same wherever I am, even when I'm outside the EU, e.g. in Serbia.
so if I understand this right, it could be a way to run scheme on esp32 and similar microcontrollers, isn't it?
Also its small size would make it a perfect target to compile to typescript/deno/wasm without rejecting the s-exp power and runtime possibilities in its full chicken code at the backend...
Not a scheme, but for running a lisp on microcontrollers uLisp is pretty amazing. http://www.ulisp.com/
You even get a REPL and everything WHILE running on the hardware. Super easy to set up and get going. Though as it is interpreted so you will of course not have native performance. Still very useful for prototyping and hobbyist projects.
As a rule, interpreted code has a smaller memory footprint than natively compiled programs.
Even interpreted on a several hundred MHz classic RISC microcontroller, Lisp will chew through a million cons cells a second or more - an order of magnitude or so faster than the old Lisp machines in the 80s were and they used to run giant CAD systems on those to design aircraft and stuff. (Albeit slowly...)
OTOH if you want something that gives you a REPL and everything directly on the hardware but is also not as slow as your typical interpreter, look at Forth.
It's compiling a subset of Scheme that can be statically typed. It's not for full-blown live-hackable Scheme programs. You'd use Crunch or PreScheme to implement things that you can't implement in Scheme, like a garbage collector. I don't know if Crunch has this feature, but with PreScheme you can run your PreScheme programs at the Scheme REPL so you can have your comfy REPL-driven dev environment and then create a static executable when you're ready.
This happened to me with idris and many others, I took some time to learn the basics, wrote some examples and then FFI was a joke or code generators for JavaScript absolutely useless.
So no way of leveraging an existing ecosystem.
reply