As a pupil of Dijkstra and seeing at least some rise in formal verification because of the modern tooling and as a follower of Lean (and Agda, Coq, Idris* etc), I hope it will be at least a strive to deliver parts of proofs in code verifiable form. More machine verifiable building blocks will lead to a bettering of everything.

▲

Imustaskforhelp 5 days ago | parent | next [-]

Offtopic, but I am 17 too just like Hannah Cairo but nothing too groundbreaking till now I suppose and it absolutely brings me delight that I can talk to somebody who was a pupil of Dijkstra, I have heard a lot about dijkstra's algorithm's and I had forgotten about it and so I searched it right now, but the only thing I knew is that it is pretty popular algorithm.

If I had to ask you kind sir, what would be the biggest life lesson (in coding, or anything general) that you could give me be?

▲

Timwi 5 days ago | parent | next [-]

> what would be the biggest life lesson (in coding, or anything general)

Pursue what interests you and what fires up your passion, not what grown-ups tell you is “lucrative”, “prestigious”, “profitable” or somesuch.

	▲	Imustaskforhelp 4 days ago \| parent \| next [-]
		I mean, my interests are just really niche in the sense that I like to glue projects and one of my favourite hobbies is to search if there is an open source replacement to something or if I can use open source things to do stuff So there is intel tiber cloud and it gave me a free jupyter and I wanted to play minecraft server, so I went to something which is a fork of it and I saw that there was a guy who had created rootless patch of ssh but it wasn't working for me so I kindly asked them and they were really kind enough to help me and then I used something like pinggy or the thousand other cloudflare tunnel-esque solutions which work without any problem whatsoever directly through ssh Earlier I used to use junest to then get something like ssh working. Can I be honest? I am so proud of myself because I guess I did all this stuff an year ago but I still remember the day I asked my friend to join the mc server and I joined too, the ping sucked but 8 gigs ram or even more and no storage limits and complete freedom... and I thought of such stuff after almost 2 weeks of trying different things and learned a lot about nat punching etc. So such stuff always makes really sense to me, just tinkering with software. But I feel like I need to create some professional software too in order to leave a legacy or just, I feel like, if I am being honest, that the things that I am doing aren't that valuable. Anybody can learn such stuff from me from some blog post I write but there is nothing that I can ever monetize. I don't know why I am seeking monetization that much but its just that, I see all these kids hustling my age too and I feel like everyone's doing everything for the money... so why should I be any different. I get a lot of ideas but I feel like I can never earn a single cent out of it and I find it a little frustating. I feel less confident myself regarding if I will ever earn decent money or will just be a low level cog of this whole system. Found it https://github.com/mkj/dropbear I really love this project so much, it really helped me do something really wonderful.
	▲	anonzzzies 4 days ago \| parent \| prev [-]
		I have nothing to add to that.

▲

lsuresh 4 days ago | parent | prev [-]

Not the one you asked, but here's what I would have told my 17 year old self.

* "Slope beats y-intercept." The best computer scientists and engineers I've ever worked with and/or mentored embodied this principle more than anything else.

* It can be tempting to over-optimize for short-term milestones (e.g., an important admissions exam, the next job or promotion), but there is a significant compounding value to knowledge accumulation and truly learning your craft well. Read and learn as much as you can, all the time, even if it isn't immediately necessary or useful.

▲

valenterry 5 days ago | parent | prev [-]

I'm on the practical side of things and have dabbled quite a bit with languages like Idris, I think we are mostly far from using them because of ergonomics.

Even in Scala (which is a very advanced language, but still far behind Idris) I deliberately don't use certain type-level features because it increases the compilation times too much (even with incremental compile!). It's very sad, but this is reality.

So, the problem isn't really that we need to "invent airplanes" - we already have them! What we need to do is make them usable and affordable by everyone.

I see more and more languages trying to add type-level features or try to embed other languages like Prolog-like ones into them. I hope that gets traction and becomes ergonomic, otherwise no one will use it in practice.

	▲	anonzzzies 5 days ago \| parent [-]
		I agree; I would say that most can be taught to people without advanced math/logic degrees/backgrounds, but because the tools are created by (and usually for) people with formal verification majors), they are just quite bad ergonomically as you say. I think we are in a good place of making it these types of proofs easier and faster more mainstream effort, not just one professor and their students, is put behind it. I believe AI will play a part here.